DocumentCode :
900319
Title :
A Verifiable Language for Programming Real-Time Communication Schedules
Author :
Fischmeister, Sebastian ; Sokolsky, Oleg ; Lee, Insup
Author_Institution :
Univ. of Pennsylvania, Philadelphia
Volume :
56
Issue :
11
fYear :
2007
Firstpage :
1505
Lastpage :
1519
Abstract :
Distributed hard real-time systems require predictable communication at the network level and verifiable communication behavior at the application level. At the network level, communication between nodes must be guaranteed to happen within bounded time and one common approach is to restrict the network access by enforcing a time-division multiple access (TDMA) schedule. At the application level, the application´s communication behavior should be verified to ensure that the application uses the predictable communication in the intended way. Network code is a domain-specific programming language to write a predictable verifiable distributed communication for distributed real-time applications. In this paper, we present the syntax and semantics of network code, how we can implement different scheduling policies, and how we can use tools such as model checking to formally verify the properties of network code programs. We also present an implementation of a runtime system for executing network code on top of RTLinux and measure the overhead incurred from the runtime system.
Keywords :
computer networks; program verification; programming languages; real-time systems; telecommunication computing; time division multiple access; RTLinux; domain-specific programming language; network code; network code programs; network code semantics; network code syntax; real-time communication; time-division multiple access; verifiable distributed communication; verifiable language; Application software; Communication system control; Computer languages; Control systems; Electrical equipment industry; Industrial control; Job shop scheduling; Real time systems; Time division multiple access; Timing; Networks; Real time systems; Scheduling; Software verification and validation; Time division multiaccess;
fLanguage :
English
Journal_Title :
Computers, IEEE Transactions on
Publisher :
ieee
ISSN :
0018-9340
Type :
jour
DOI :
10.1109/TC.2007.70747
Filename :
4336299
Link To Document :
بازگشت