Semantics for Communicating Actors with Interdependent Real-Time Deadlines

Istvan Knoll, Anders Peter Ravn, Arne Skou

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelProceedings of Third IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009.
ForlagIEEE Computer Society Press
Publikationsdato2009
Sider29-35
ISBN (Trykt)978-0-7695-3757-3
DOI
StatusUdgivet - 2009
BegivenhedThird IEEE International Symposium on Theoretical Aspects of Software Engineering - Tianjin, Kina
Varighed: 29 jul. 200931 jul. 2009

Konference

KonferenceThird IEEE International Symposium on Theoretical Aspects of Software Engineering
LandKina
ByTianjin
Periode29/07/200931/07/2009

Emneord

  • Embedded systems

Fingeraftryk Dyk ned i forskningsemnerne om 'Semantics for Communicating Actors with Interdependent Real-Time Deadlines'. Sammen danner de et unikt fingeraftryk.

Citationsformater