Electronic Resource
Springer
Annals of software engineering
7 (1999), S. 127-155
ISSN:
1573-7489
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementing real-time semantics using dynamic priorities. For this purpose a process algebra with dynamic priority is defined, whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior. The utility of the technique is demonstrated by a case study that deals with the formal modeling and verification of several aspects of the widely-used SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra with dynamic priority is implemented. It turns out that the state space of the bus-protocol model is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus protocol.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1018982020561
Permalink
|
Location |
Call Number |
Expected |
Availability |