Generalized interface automata with multicast synchronization

doi:10.1007/s11704-014-4016-7

Front. Comput. Sci.

2015, Vol. 9

Issue (1) : 1-14 https://doi.org/10.1007/s11704-014-4016-7

RESEARCH ARTICLE

Generalized interface automata with multicast synchronization

Fei HE^1,^2,^3,^*(

),Xiaoyu SONG⁴,Ming GU^1,^2,³,Jiaguang SUN^1,^2,³

1. Tsinghua National Laboratory for Information Science and Technology (TNList), Tsinghua University, Beijing 100084, China
2. Key Laboratory for Information System Security, Ministry of Education, Beijing 100084, China
3. School of Software, Tsinghua University, Beijing 100084, China
4. Department of Electrical & Computer Engineering, Portland State University, Oregon 97207, USA

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

Abstract

Interface automata are one of the prominent formalisms for specifying interface behaviors of componentbased systems. However, only one-to-one communication is allowed in the composition of interface automata. This paper presents multicast interface automata which generalize the classic interface automata and accommodate multicast communication mechanism. The multicast interface automata endorse both bottom-up and top-down design methodologies. Theoretical results on compatibility and refinement are established for incremental design and independent implementability.

Keywords interface automata multicast communication component interaction verification

Corresponding Author(s): Fei HE

Issue Date: 09 February 2015

Cite this article:

Fei HE,Xiaoyu SONG,Ming GU, et al. Generalized interface automata with multicast synchronization[J]. Front. Comput. Sci., 2015, 9(1): 1-14.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-014-4016-7
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I1/1

1	Alfaro L D, Henzinger T A. Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 2001, 109-120
2	Alfaro L D, Henzinger T A. Interface-based design. Engineering Theories of Software-intensive Systems, 2005, 195: 83-104 https://doi.org/10.1007/1-4020-3532-2_3
3	Lynch N A, Tuttle M R. Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing. 1987, 137-151
4	Lynch N A, Tuttle M R. An introduction to input/output automata. CWI-Quarterly, 1989, 2(3): 219-246
5	Lynch N A. Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo, CA, 1996.
6	Kaynar D K, Lynch N A, Segala R, Vaandrager F. Timed I/O automata: a mathematical framework for modeling and analyzing realtime systems. In: Proceedings of the 24th IEEE Real-Time Systems Symposium. 2003, 166-177
7	Kaynar D K, Lynch N A, Segala R, Vaandrager F. The theory of timed I/O automata. Synthesis Lectures on Computer Science, 2006, 1(1): 1-114 https://doi.org/10.2200/S00006ED1V01Y200508CSL001
8	Wu S H, Smolka S A, Stark E W. Composition and behaviors of probabilistic I/O automata. Theoretical Computer Science, 1997, 176(1-2): 1-38 https://doi.org/10.1016/S0304-3975(97)00056-X
9	Stark E W, Smolka S A. Compositional analysis of expected delays in networks of probabilistic I/O automata. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. 1998, 466-477
10	Stark E W, Cleaveland R, Smolka S A. A process-algebraic language for probabilistic I/O automata. Lecture Notes in Computer Science, 2003, 2761: 193-207 https://doi.org/10.1007/978-3-540-45187-7_13
11	Lynch N A, Segala R, Vaandrager F W. Hybrid I/O automata. Information and Computation, 2003, 185(1): 105-157 https://doi.org/10.1016/S0890-5401(03)00067-1
12	Alfaro L D, Henzinger T A. Interface theories for component based design. Lecture Notes in Computer Science, 2001, 2211: 148-165 https://doi.org/10.1007/3-540-45449-7_11
13	Wen Y J, Wang J, Qi Z C. Bridging refinement of interface automata to forward simulation of I/O automata. In: Proceedings of the 6th International Conference on Formal Engineering Methods. 2004, 259-273
14	Wen Y J, Wang J, Qi Z C. 2/3 alternating simulation between interface automata. In: Proceedings of 7th International Conference on Formal Engineering Methods. 2005, 173-187.
15	Chakrabarti A, Alfaro L D, Henzinger T A, Jurdzinski M, Mang F Y C. Interface compatibility checking for software modules. Lecture Notes in Computer Science, 2002, 2404: 428-441 https://doi.org/10.1007/3-540-45657-0_35
16	Chakrabarti A, Alfaro L D, Henzinger T A, Mang F Y C. Synchronous and bidirectional component interfaces. Lecture Notes in Computer Science, 2002, 2404: 414-427 https://doi.org/10.1007/3-540-45657-0_34
17	Alfaro L D, Henzinger T A, Stoelinga M. Timed interfaces. Lecture Notes in Computer Science, 2002, 2491: 108-122 https://doi.org/10.1007/3-540-45828-X_9
18	Chakrabarti A, Alfaro L D, Henzinger T A, Stoelinga M. Resource interfaces. Lecture Notes in Computer Science, 2003, 2855: 117-133 https://doi.org/10.1007/978-3-540-45212-6_9
19	Alfaro L D, Silva L D D, Faella M, Legay A, Roy P, Sorea M. Sociable interfaces. Lecture Notes in Computer Science, 2005, 3717: 81-105 https://doi.org/10.1007/11559306_5
20	Alur R, Henzinger T A, Kupferman O, Vardi M. Alternating refinement relations. Lecture Notes in Computer Science, 1998, 1466: 163-178 https://doi.org/10.1007/BFb0055622

[1]

Supplementary Material

Download

[1]	Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[2]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[3]	Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[4]	Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[5]	Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[6]	Ruifeng XU,Lin GUI,Qin LU,Shuai WANG,Jian XU. Incorporating multi-kernel function and Internet verification for Chinese person name disambiguation[J]. Front. Comput. Sci., 2016, 10(6): 1026-1038.
[7]	Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[8]	Yu ZHOU,Yankai HUANG,Ou WEI,Zhiqiu HUANG. Verifying specifications with associated attributes in graph transformation systems[J]. Front. Comput. Sci., 2015, 9(3): 364-374.
[9]	Xuzhou LI,Yilong YIN,Yanbin NING,Gongping YANG,Lei PAN. A hybrid biometric identification framework for high security applications[J]. Front. Comput. Sci., 2015, 9(3): 392-401.
[10]	Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[11]	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.
[12]	Jean-Vivien MILLO, Frédéric MALLET, Anthony COADOU, S RAMESH. Scenario-based verification in presence of variability using a synchronous approach[J]. Front Comput Sci, 2013, 7(5): 650-672.
[13]	Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Lo?c BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front Comput Sci, 2013, 7(5): 598-616.
[14]	Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
[15]	Yuehua DAI, Yi SHI, Yong QI, Jianbao REN, Peijian WANG. Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture[J]. Front Comput Sci, 2013, 7(1): 34-43.

Viewed

Full text

Abstract

Cited

Shared

Discussed