Semantics for Communicating Actors with Interdependent Real-Time Deadlines

Publication: Research - peer-reviewArticle in proceeding

Abstract

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.
Close

Details

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.
Original languageEnglish
Title of host publicationProceedings of Third IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009.
PublisherIEEE Computer Society Press
Publication date2009
Pages29-35
ISBN (print)978-0-7695-3757-3
DOI
StatePublished - 2009
Event - Tianjin, China

Conference

ConferenceThird IEEE International Symposium on Theoretical Aspects of Software Engineering
LandChina
ByTianjin
Periode29/07/200931/07/2009

    Keywords

  • Embedded systems, Semantics, Real-Time
ID: 18489814