DESCRIPTIVE FORMAL METHODS

 

LOGICS

1. Examples of Required Properties

The gate must be closed when a train passes the crossing.

If the library has a requested book and it is not on loan,

then find its shelf location.

All planes must maintain a minimum separation distance.

2. Propositional Logic (Boolean Algebra)

Truth-Valued Variables + {T, F} + Logical Connectives

( Trains_In Þ Gate_Closed ) Ù ( ØTrains_In Þ Gate_Open )

3. Predicate Logic (First Order Logic)

Add Functions, General Variables, and Quantifiers (" , $ ).

"count ((count > 0 Þ Gate_Closed) Ù (count=0 Þ Gate_Open))

Invariants, Preconditions, Postconditions

{ Pre(i1, ..., in) } Function { Post(o1, ..., om, i1, ..., in) }

4. Temporal Logic

Assertions on States and Sequences of States

Add Eventually (à ) , Always ( [] ), and Until (u ) Operators.

[] ( count > 0 Þ à Gate_Closed )

5. Real-Time Logic (Jahanian & Mok)

First Order Logic + Timed Events

Event Occurrence Function @

@ : Event_Class ´ Instance_Integer® Time_of_Occurrence

e.g., @(Press_Start_Button, 10) =

Time of the 10th Instance of the Press_Start_Button Event.