| Question |
|
|
|
|
|
|
|
|
|
|
|
|
|
| • | So we
have a big statecharts-like specification |
|||||||||||
| • | How
do we know it has properties we want it to |
|||||||||||
| have? |
||||||||||||
| – | Ex:
is it deterministic? |
|||||||||||
| – | Ex:
can you ever have the doors unlock by themselves |
|||||||||||
| while
the car is moving? |
||||||||||||
| – | Ex:
can you ever cause an emergency descent when you |
|||||||||||
| are
under 500 feet above ground level? |
||||||||||||
