|
|
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 |
|
|
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
|
|
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|