Verification of a Heterogeneous Model with Temporal Properties
Chihhong Patrick Cheng and Edward A. Lee
PTIDES  is a distributed DE model that binds model time to physical time at the ports of sensors and actuators; for events at an actuator port, PTIDES can guarantee that they are received by the actor port prior to the time stamp of the event.
Formal verification tries to examine whether the model satisfies a specification. LTL, S1S, CTL* are temporal logics that describe the behavior for state transition systems (either finite or infinite). There are also extensions of real time logic that explicitly describe the interval between states. Model checking in real time models is possible. Thus we are investigating how to leverage these temporal logics to verify PTIDES designs. Two main technical challenges would emerge. Modeling discrete-event (DE) behavior with transition systems is the first challenge. Representing the temporal properties for tractable verification is the second.
In this project, we expect to achieve the following goals:
- Model Construction:
Model discrete-event (DE) behavior with transition systems;
- Behavioral Description:
Use existing temporal logic to describe some allowable behaviors in the spec;
- Model Checking:
Apply suitable model checking techniques to the model. Also find suitable examples as testcases; and
Use simulation or abstraction refinement techniques to check whether the violation of a specification is a false positive.
- Y. Zhao, E. A. Lee, and J. Liu, Programming Temporally Integrated Distributed Embedded Systems, UC Berkeley EECS Technical Report UCB/EECS-2006-82, May 28 2006.