Dynamic input/output automata: A formal and compositional model for dynamic systems

被引:11
作者
Attie, Paul C. [1 ]
Lynch, Nancy A. [2 ]
机构
[1] Amer Univ Beirut, Dept Comp Sci, Beirut, Lebanon
[2] MIT Comp Sci & Artificial Intelligence Lab, Cambridge, MA USA
关键词
Dynamic systems; Formal methods; Semantics; Automata; Process creation; Mobility; VERIFICATION; SERVICE;
D O I
10.1016/j.ic.2016.03.008
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present dynamic I/O automata (DIOA), a compositional model of dynamic systems. In DIOA, automata can be created and destroyed dynamically, as computation proceeds, and an automaton can dynamically change its signature, i.e., the set of actions in which it can participate. DIOA features operators for parallel composition, action hiding, action renaming, a notion of automaton creation, and a notion of behavioral subtyping by means of trace inclusion. DIOA can model mobility, using signature modification, and is hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. We also show that parallel composition, action hiding, action renaming, and (subject to some technical conditions) automaton creation are all monotonic with respect to trace inclusion: if one component is replaced by another whose traces are a subset of the former, then the set of traces of the system as a whole can only be reduced. (C) 2016 Elsevier Inc. All rights reserved.
引用
收藏
页码:28 / 75
页数:48
相关论文
共 31 条
[1]   Reactive modules [J].
Alur, R ;
Henzinger, TA .
FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (01) :7-48
[2]  
[Anonymous], 2002, MITLCSTR868
[3]  
[Anonymous], 1989, CWI-Quarterly
[4]  
[Anonymous], 1996, Distributed algorithms
[5]  
Araragi T., 2000, LECT NOTES ARTIF INT, V1871, P48
[6]   On the refinement of liveness properties of distributed systems [J].
Attie, Paul C. .
FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (01) :1-46
[7]   Rigorous Component-Based System Design Using the BIP Framework [J].
Basu, Ananda ;
Bensalem, Saddek ;
Bozga, Marius ;
Combaz, Jacques ;
Jaber, Mohamad ;
Thanh-Hung Nguyen ;
Sifakis, Joseph .
IEEE SOFTWARE, 2011, 28 (03) :41-48
[8]   A framework for automated distributed implementation of component-based models [J].
Bonakdarpour, Borzoo ;
Bozga, Marius ;
Jaber, Mohamad ;
Quilbeuf, Jean ;
Sifakis, Joseph .
DISTRIBUTED COMPUTING, 2012, 25 (05) :383-409
[9]  
Bozga Marius, 2012, Software Composition. Proceedings 11th International Conference, SC 2012, P1, DOI 10.1007/978-3-642-30564-1_1
[10]   Mobile ambients [J].
Cardelli, L ;
Gordon, AD .
THEORETICAL COMPUTER SCIENCE, 2000, 240 (01) :177-213