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

doi:10.1007/s11704-014-4096-4

Front. Comput. Sci.

2015, Vol. 9

Issue (1) : 87-110 https://doi.org/10.1007/s11704-014-4096-4

RESEARCH ARTICLE

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

Yanwen CHEN^1,^2,³(

),Yixiang CHEN^1,^*(

),Eric MADELAINE^2,³

1. MoE Engineering Research Center for Software/Hardware Co-design Technology and Application, Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
2. INRIA Sophia Antipolis Méditérannée, Sophia Antipolis 06902, France
3. University of Nice Sophia Antipolis, CNRS, Sophia Antipolis 06900, France

Download: PDF(1006 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Yixiang CHEN

Issue Date: 09 February 2015

Cite this article:

Yanwen CHEN,Yixiang CHEN,Eric MADELAINE. Timed-pNets: a communication behavioural semantic model for distributed systems[J]. Front. Comput. Sci., 2015, 9(1): 87-110.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-014-4096-4
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I1/87

1	Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558-565 https://doi.org/10.1145/359545.359563
2	Fidge C. Logical time in distributed computing systems. Computer, 1991, 24(8): 28-33 https://doi.org/10.1109/2.84874
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 https://doi.org/10.1016/0167-6423(91)90001-E
5	Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293-1304 https://doi.org/10.1109/5.97299
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 https://doi.org/10.1007/s12243-008-0069-7
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 https://doi.org/10.1007/978-3-642-30561-0_4
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 https://doi.org/10.1016/j.ic.2008.12.004
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 https://doi.org/10.1109/40.296155
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 https://doi.org/10.1145/2093328.2093337
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 https://doi.org/10.1016/0304-3975(94)90010-8
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 https://doi.org/10.1007/11663430_7
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 https://doi.org/10.1109/JPROC.2011.2161237
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 https://doi.org/10.1109/TASE.2013.16
29	He J. A Clock-based framework for construction of hybrid systems. Lecture Notes in Computer Science, 2013, 8049: 22-41 https://doi.org/10.1007/978-3-642-39718-9_2
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

[1]

Supplementary Material

Download

[1]	Zhenxue HE, Limin XIAO, Fei GU, Li RUAN, Zhisheng HUO, Mingzhe LI, Mingfa ZHU, Longbing ZHANG, Rui LIU, Xiang WANG. EDOA: an efficient delay optimization approach for mixed-polarity Reed-Muller logic circuits under the unit delay model[J]. Front. Comput. Sci., 2019, 13(5): 1102-1115.
[2]	Kai HU, Zhangbo DUAN, Jiye WANG, Lingchao GAO, Lihong SHANG. Template-based AADL automatic code generation[J]. Front. Comput. Sci., 2019, 13(4): 698-714.
[3]	Xiaobing SUN, Hui YANG, Hareton LEUNG, Bin LI, Hanchao (Jerry) LI, Lingzhi LIAO. Effectiveness of exploring historical commits for developer recommendation: an empirical study[J]. Front. Comput. Sci., 2018, 12(3): 528-544.
[4]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[5]	Zheng FU, Graeme SMITH. Property transformation under specification change[J]. Front Comput Sci Chin, 2011, 5(1): 1-13.

Viewed

Full text

Abstract

Cited

Shared

Discussed