Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

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 HE1,2,3,*(),Xiaoyu SONG4,Ming GU1,2,3,Jiaguang SUN1,2,3
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