Specification and Validation of a Dynamically Reconfigurable System

Kaoru TAKAHASHI  Toshihiko ANDO  Toshihisa KANO  Goichi ITABASHI  Yasushi KATO  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E81-A   No.4   pp.556-565
Publication Date: 1998/04/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Concurrent Systems Technology)
Category: 
Keyword: 
distributed concurrent systems,  dynamically reconfigurable systems,   formal specification,  formal validation,  communicating finite state machines,   simulator,  validator,  

Full Text: PDF(1003.7KB)>>
Buy this Article




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.