This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Verifiable Language for Programming Real-Time Communication Schedules
November 2007 (vol. 56 no. 11)
pp. 1505-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 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 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 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 run-time system.

[1] T.A. Henzinger and C.M. Kirsch, “The Embedded Machine: Predictable, Portable Real-Time Code,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 315-326, 2002.
[2] M. Anand, S. Fischmeister, and I. Lee, “An Analysis Framework for Network-Code Programs,” Proc. Sixth Ann. ACM Conf. Embedded Software (EmSoft '06), 2006.
[3] S. Fischmeister, O. Sokolsky, and I. Lee, “Appendix: Programmable Real-Time Communication Schedules,” technical report, Univ. of Pennsylvania, 2005.
[4] S. Fischmeister, “Multi-Dimensional Schedules for Media-Access Control in Time-Triggered Communication,” Proc. 10th IEEE Symp. Computers and Comm. (ISCC '05), 2005.
[5] D. Clark, K. Pogran, and D. Reed, “An Introduction to Local Area Networks,” Proc. IEEE, vol. 66, pp. 1497-1517, Nov. 1978.
[6] C. Venkatramani and T. Chiueh, “Design, Implementation, and Evaluation of a Software-Based Real-Time Ethernet Protocol,” Proc. Conf. Applications, Technologies, Architectures, and Protocols for Computer Comm. (SIGCOMM '95), pp. 27-37, 1995.
[7] D. Clarke, I. Lee, and H.-L. Xie, “VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems,” J. Computer and Software Eng., vol. 3, pp. 185-215, Apr. 1995.
[8] I. Lee, P. Brémond-Grégoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems,” Proc. IEEE, pp. 158-171, Jan. 1994.
[9] J.-Y. Choi, I. Lee, and H.-L. Xie, “The Specification and Schedulability Analysis of Real-Time Systems Using ACSR,” Proc. 16th IEEE Real-Time Systems Symp. (RTSS '95), Dec. 1995.
[10] M. Bozga, S. Graf, I. Ober, I. Ober, and J. Sifakis, “Tools and Applications: The IF Toolset,” Proc. Fourth Int'l School on Formal Methods for the Design of Computer, Comm., and Software Systems: Real Time (SFM-04:RT), M. Bernanrdo and F. Corradini, eds., 2004.
[11] A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P.L. Guernic, and R. de Simone, “The Synchronous Languages Twelve Years Later,” Proc. IEEE, special issue on embedded systems, vol. 91, pp.64-83, Jan. 2003.
[12] M. Anand, S. Fischmeister, and J. Kim, “Distributed Code Generation from Hybrid Systems Models for Time-Delayed Multirate Systems,” Proc. Fifth ACM Conf. Embedded Software (EmSoft '05), 2005.
[13] H. Kopetz, “TTP/A The Fireworks Protocol,” Proc. SAE Int'l Congress and Exposition, Feb. 1995.
[14] J. Elson, L. Girod, D. Estrin, B. Simons, J. Welch, and N. Lynch, “An Overview of Clock Synchronization,” Fault-Tolerant Distributed Computing, B. Simons and A. Spector, eds., pp. 84-96, Springer, 1990.
[15] E. Anceaume and I. Puaut, “Performance Evaluation of Clock Synchronization Algorithms, ” technical report, INRIA, Oct. 1998.
[16] H. Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications. Kluwer Academic, 1997.
[17] S. Eberle, C. Ebner, W. Elmenreich, G. Färber, P. Göhner, W. Haidinger, M. Holzmann, R. Huber, R. Schlatterbeck, H. Kopetz, and A. Stothert, Specification of the TTP/A Protocol v2.00, Research Report 61/2001, Institut für Technische Informatik, Technische Universität Wien, pp. 1-3/182-1, 2001.
[18] T. Führer, B. Müller, W. Dieterle, F. Hartwich, R. Hugel, and M. Walther, “Time Triggered Communications on CAN (Time Triggered CAN-TTCAN),” Proc. Seventh Int'l CAN Conf., 2000.
[19] F. Consortium, FlexRay Communications System—Protocol Specification, version 2.0, June 2004.
[20] J. Ferreira, P. Pedreiras, L. Almeida, and J. Fonseca, “The FTT-CAN Protocol for Flexibility in Safety-Critical Systems,” IEEE Micro, vol. 22, no. 4, pp. 46-55, July-Aug. 2002.
[21] P. Pedreiras, L. Almeida, and P. Gai, “The FTT-Ethernet Protocol: Merging Flexibility, Timeliness and Efficiency,” Proc. 14th Euromicro Conf. Real-Time Systems (ECRTS '02), pp. 134-142, June 2002.
[22] “Ethernet Powerlink: Data Transport Services,” white paper, Bernecker + Rainer Industrie Elektronik, fifth ed., Sept. 2002.
[23] F. Hanssen and P. Jansen, “Real-Time Communication Protocols: An Overview,” technical report, Centre for Telematics and Information Tech nology, 2003.
[24] J. Kiszka, B. Wagner, Y. Zhang, and J. Broenink, “RTnet—A Flexible Hard Real-Time Networking Framework,” Proc. 10th IEEE Int'l Conf. Emerging Technologies and Factory Automation (ETFA '05), 2005.
[25] G. König, “Using Interpreters for Scheduling Network Communication in Distributed Real-Time Systems,” master's thesis, Salzburg Univ., Mar. 2005.
[26] P.C. Ölveczky and J. Meseguer, “Specification and Analysis of Real-Time Systems Using Real-Time Maude,” Proc. Fundamental Aspects of Software Eng. (FASE '04), 2004.
[27] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, “Times: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems,” Proc. First Int'l Workshop Formal Modeling and Analysis of Timed Systems (FORMATS '03), P. Niebert and K.G.Larsen, eds., pp. 60-72, 2004.

Index Terms:
Real time systems, Scheduling, Time division multiaccess, Networks, Software verification and validation
Citation:
Sebastian Fischmeister, Oleg Sokolsky, Insup Lee, "A Verifiable Language for Programming Real-Time Communication Schedules," IEEE Transactions on Computers, vol. 56, no. 11, pp. 1505-1519, Nov. 2007, doi:10.1109/TC.2007.70747
Usage of this product signifies your acceptance of the Terms of Use.