Timed-pNets: a communication behavioural semantic model for distributed systems

Abstract

This paper presents an approach to build a communication behavioural semantic model for heterogeneous distributed systems that include synchronous and asynchronous communications. Since each node of such system has its own physical clock, it brings the challenges of correctly specifying the system time constraints. Based on the logical clocks proposed by Lamport, and CCSL proposed by Aoste team in INRIA, as well as pNets from Oasis team in INRIA, we develop timed-pNets to model communication behaviours for distributed systems. Timed-pNets are tree style hierarchical structures. Each node is associated with a timed specification which consists of a set of logical clocks and some relations on clocks. The leaves are represented by timed-pLTSs. Non-leaf nodes (called timed-pNets nodes) are synchronisation devices that synchronize the behaviours of subnets (these subnets can be leaves or non-leaf nodes). Both timed-pLTSs and timed-pNets nodes can be translated to timed specifications. All these notions and methods are illustrated on a simple use-case of car insertion from the area of intelligent transportation systems (ITS). In the end the TimeSquare tool is used to simulate and check the validity of our model.

Keywords

ITS / logical time / formal method / timed specification / synchronous and asynchronous communication

References

[1] Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558-565

[2] Fidge C. Logical time in distributed computing systems. Computer, 1991, 24(8): 28-33

[3] Berry G. The foundations of esterel. In: Proceedings of Proof, Language, and Interaction. 2000, 425-454

[4] Benveniste A, Le Guernic P, Jacquemot C. Synchronous programming with events and relations: the signal language and its semantics. Science of computer programming, 1991, 16(2): 103-149

[5] Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293-1304

[6] André C. Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925, INRIA, 2009 (in French)

[7] Barros T, Boulifa R, Cansado A, Henrio L, Madelaine E. Behavioural models for distributed Fractal components. Annals of Telecommunications, 2009, 64(1-2): 25-43

[8] Arnold A, Plaice J. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall International (UK) Ltd., 1994

[9] Ameur-Boulifa R, Henrio L, Madelaine E, Savu A. Behavioural Semantics for Asynchronous Components. Research Report RR-8167, INRIA, 2012 (in French)

[10] Chen Y, Chen Y, Madelaine E. Timed-pNets: a formal communication behavior model for real-time CPS systems. In: Proceedings of Workshop on Trustworthy Cyber Physical Systems. 2012

[11] Deantoni J, Mallet F. TimeSquare: Treat your models with logical time. In: Proceedings of the 50th International Conference on Objects, Models, Components, Patterns. 2012, 34-41

[12] Milner R. Communicating and Mobile Systems: the π-Calculus. New York: Cambridge University Press, 1999

[13] Milner R. Communication and Concurrency. Prentice-Hall, Inc., 1989

[14] Cansado A, Madelaine E. Specification and verification for grid component-based applications: from models to tools. In: Proceedings of Formal Methods for Components and Objects. 2009, 180-203

[15] Caromel D, Henrio L, Serpette B P. Asynchronous sequential processes. Information and Computation, 2008, 207(4): 459-495

[16] Bulirsch R, Stoer J. Introduction to Numerical Analysis. Springer Heidelberg, 2002

[17] Chapiro D M. Globally-asynchronous locally-synchronous systems. Dissertation for the Doctoral Degree. California: Stanford University. 1984

[18] Chiodo M, Giusto P, Jurecska A, Hsieh H C, Sangiovanni-Vincentelli A, Lavagno L. Hardware-software codesign of embedded systems. IEEE Micro, 1994, 14(4): 26-36

[19] Berry G, Nicolas C, Serrano M. Hiphop: a synchronous reactive extension for hop. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients. 2011, 49-56

[20] Berry G, Sentovich E. Multiclock esterel. In: Proceedings of Correct Hardware Design and Verification Methods. 2001, 110-125

[21] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183-235

[22] Bengtsson J, Larsen K G, Larsson F, Pettersson P, Yi W. Uppaal — a tool suite for automatic verification of real–time systems. In: Proceedings of Workshop on Verification and Control of Hybrid Systems III, LNCS 1066. 1995, 232-243

[23] Basu A, Bozga M, Sifakis J. Modeling heterogeneous real-time components in BIP. In: Proceedings of the 4th IEEE International Conference on Software Engineering and Formal Methods. 2006, 3-12

[24] Graf S, Gérard S, Haugen Ø, Ober L, Selic B. Modeling and analysis of real-time and embedded system. Lecture Notes in Computer Science, 2006, 3844: 58-66

[25] Eidson J, Lee E A, Matic S, Seshia S A, Zou J. Distributed real-time software for cyber-physical systems. Proceedings of the IEEE (special issue on CPS), 2012, 100(1): 45-59

[26] Valero Ruiz V, Frutos Escrig d D, Cuartero Gomez F. On nondecidability of reachability for timed-arc Petri nets. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models. 1999, 188-196

[27] Chen Y. Stec: a location-triggered specification language for real-time systems. In: Proceedings of the ISORC Workshops. 2012, 1-6

[28] Wu H, Chen Y, Zhang M. On denotational semantics of spatialtemporal consistency language–Stec. In: Proceedings of the 2013 International Symposium on Theoretical Aspects of Software Engineering. 2013, 113-120

[29] He J. A Clock-based framework for construction of hybrid systems. Lecture Notes in Computer Science, 2013, 8049: 22-41

[30] Chen Y, Zhang Y. A hybrid clock system related to STeC language. In: Proceeding<?Pub Caret?>s of the 8th International Conference on Software Security and Reliability. 2014, 199-203

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg