A Practical Approach to Implementing Real-Time Semantics

Luettgen, Gerald; Bhat, Girish; Cleaveland, Rance

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 proces 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 which deals with the formal modeling and verification of the 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.

Document ID

19990021369

Acquisition Source

Langley Research Center

Document Type

Preprint (Draft being sent to journal)

Authors

Date Acquired

September 6, 2013

Publication Date

January 1, 1999

Subject Category

Report/Patent Number

Funding Number(s)

Distribution Limits

Public

Work of the US Gov. Public Use Permitted.

Available Downloads

Name

Type

19990021369.pdf

STI

No Preview Available

NTRS

NTRS - NASA Technical Reports Server

Available Downloads

Related Records