Specification and Validation of a Dynamically Reconfigurable System
Summary :
In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E81-A No.4 pp.556-565
- Publication Date
- 1998/04/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Concurrent Systems Technology)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kaoru TAKAHASHI, Toshihiko ANDO, Toshihisa KANO, Goichi ITABASHI, Yasushi KATO, "Specification and Validation of a Dynamically Reconfigurable System" in IEICE TRANSACTIONS on Fundamentals,
vol. E81-A, no. 4, pp. 556-565, April 1998, doi: .
Abstract: In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e81-a_4_556/_p
Copy
@ARTICLE{e81-a_4_556,
author={Kaoru TAKAHASHI, Toshihiko ANDO, Toshihisa KANO, Goichi ITABASHI, Yasushi KATO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Specification and Validation of a Dynamically Reconfigurable System},
year={1998},
volume={E81-A},
number={4},
pages={556-565},
abstract={In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.},
keywords={},
doi={},
ISSN={},
month={April},}
Copy
TY - JOUR
TI - Specification and Validation of a Dynamically Reconfigurable System
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 556
EP - 565
AU - Kaoru TAKAHASHI
AU - Toshihiko ANDO
AU - Toshihisa KANO
AU - Goichi ITABASHI
AU - Yasushi KATO
PY - 1998
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E81-A
IS - 4
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - April 1998
AB - In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.
ER -
English
