Semantics for Communicating Actors with Interdependent Real-Time Deadlines

Models of embedded systems with communicating actors and deadlines offer abstraction and encapsulation of related functionality, but their behavior is complex. Verification is therefore difficult and requires a combination of simulation, model checking and testing tools. In order to rely on the results, these tools must use consistent semantics for the model. Yet, a monolithic semantic model is just as complex as the entity it describes. In order to circumvent this issue, we define a three level semantics giving independent definitions of the functionality of actors, the temporal properties of communications, and finally imposing deadlines on the timing of dependent actors. With this approach the semantics is used directly in developing a simulator supporting the nondeterminism of the abstract semantics such that e.g. potential race conditions can be detected. The layers are also planned to underpin independent specialized verification tools. The verification task for timed, hybrid systems can thus be divided into the continuous, discrete, and timing domains with automated translation to specialized tools, and this promises better scalability than simulation or model checking of one complex model.