For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Specification and Validation of a Dynamically Reconfigurable System
Kaoru TAKAHASHI Toshihiko ANDO Toshihisa KANO Goichi ITABASHI Yasushi KATO
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1998/04/25
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Concurrent Systems Technology)
distributed concurrent systems, dynamically reconfigurable systems, formal specification, formal validation, communicating finite state machines, simulator, validator,
Full Text: PDF(1003.7KB)>>
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.