Model Checking Process Algebra of Communicating Resources for Real-time Systems

Publikation: Forskning - peer reviewKonferenceartikel i proceeding

Abstrakt

This paper presents a new process algebra, called PACOR, for real-time systems which deals with resource constrained timed behavior as an improved version of the ACSR algebra. We define PACOR as a Process Algebra of Communicating Resources which allows to express preemptiveness, urgent ness and resource usage over a dense-time model. The semantic interpretation of PACOR is defined in the form of a timed transition system expressing the timed behavior and dynamic creation of processes. We define a translation of PACOR systems to Parameterized Stopwatch Automata (PSA). The translation preserves the original semantics of PACOR and enables the verification of PACOR systems using symbolic model checking in UPPAAL and statistical model checking UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.
Luk

Detaljer

This paper presents a new process algebra, called PACOR, for real-time systems which deals with resource constrained timed behavior as an improved version of the ACSR algebra. We define PACOR as a Process Algebra of Communicating Resources which allows to express preemptiveness, urgent ness and resource usage over a dense-time model. The semantic interpretation of PACOR is defined in the form of a timed transition system expressing the timed behavior and dynamic creation of processes. We define a translation of PACOR systems to Parameterized Stopwatch Automata (PSA). The translation preserves the original semantics of PACOR and enables the verification of PACOR systems using symbolic model checking in UPPAAL and statistical model checking UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.
OriginalsprogEngelsk
TitelProceedings of ECRTS 2014
UdgiverIEEE Press
Publikationsdato2014
Sider51-60
ISBN (trykt)978-1-4799-5797-2
DOI
StatusUdgivet - 2014
SerieEuromicro Conference on Real-Time Systems. Proceedings
ISSN1068-3070

Download-statistik

Ingen data tilgængelig
ID: 209589451