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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565
Fidge C. Logical time in distributed computing systems. Computer, 1991, 24(8): 28–33
Berry G. The foundations of esterel. In: Proceedings of Proof, Language, and Interaction. 2000, 425–454
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
Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293–1304
André C. Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925, INRIA, 2009 (in French)
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
Arnold A, Plaice J. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall International (UK) Ltd., 1994
Ameur-Boulifa R, Henrio L, Madelaine E, Savu A. Behavioural Semantics for Asynchronous Components. Research Report RR-8167, INRIA, 2012 (in French)
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
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
Milner R. Communicating and Mobile Systems: the π-Calculus. New York: Cambridge University Press, 1999
Milner R. Communication and Concurrency. Prentice-Hall, Inc., 1989
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
Caromel D, Henrio L, Serpette B P. Asynchronous sequential processes. Information and Computation, 2008, 207(4): 459–495
Bulirsch R, Stoer J. Introduction to Numerical Analysis. Springer Heidelberg, 2002
Chapiro D M. Globally-asynchronous locally-synchronous systems. Dissertation for the Doctoral Degree. California: Stanford University. 1984
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
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
Berry G, Sentovich E. Multiclock esterel. In: Proceedings of Correct Hardware Design and Verification Methods. 2001, 110–125
Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235
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
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
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
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
Valero Ruiz V, Frutos Escrigd D, Cuartero Gomez F. On non-decidability of reachability for timed-arc Petri nets. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models. 1999, 188–196
Chen Y. Stec: a location-triggered specification language for real-time systems. In: Proceedings of the ISORC Workshops. 2012, 1–6
Wu H, Chen Y, Zhang M. On denotational semantics of spatial-temporal consistency language-Stec. In: Proceedings of the 2013 International Symposium on Theoretical Aspects of Software Engineering. 2013, 113–120
He J. A Clock-based framework for construction of hybrid systems. Lecture Notes in Computer Science, 2013, 8049: 22–41
Chen Y, Zhang Y. A hybrid clock system related to STeC language. In: Proceedings of the 8th International Conference on Software Security and Reliability. 2014, 199–203
Author information
Authors and Affiliations
Corresponding author
Additional information
Yanwen Chen is a PhD student registed both in the East China Normal University and in the University de Nice Sophia Antipolis, France. She got her MS in both universities in the domain of computer science. Her research interests include distributed systems, cloud computing and formal methods. Now her research topic concerns the formal modeling and real-time scheduling of cyber physical systems.
Yixiang Chen is a full professor for computer science and technology at Software Engineering Institute (SEI), East China Normal University (ECNU), where he is coordinating trustworthy software, Internet of things and cloud computing related research activities. Professor Chen is the director of the Engineering Research Center for Software/Hardware Co-design Technology and Application, MoE of China. He is a Member of the Cloud Computing Experts Association of Chinese Institute of Electronics and Vice Chair of Shanghai Pudong IoT Alliance.
Eric Madelaine is a senior researcher at INRIA in Sophia-Antipolis, France. He has a diploma from Ecole Polytechnique, a PhD thesis from University of Paris 7, and an Habilitation from University of Nice, France. His research interests range from semantics of programming languages, distributed and cloud computing, component-based software, formal methods, methods and tools for specification and verification of complex programs. He has served in many international conferences committees, including Euromicro, FESCA, SEAA, FMCO, and FACS.
Rights and permissions
About this article
Cite this article
Chen, Y., Chen, Y. & Madelaine, E. Timed-pNets: a communication behavioural semantic model for distributed systems. Front. Comput. Sci. 9, 87–110 (2015). https://doi.org/10.1007/s11704-014-4096-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11704-014-4096-4