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.