A Topological Framework of Stepwise Specification for Concurrent Systems

Toshihiko ANDO
Kaoru TAKAHASHI
Yasushi KATO

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E79-A    No.11    pp.1760-1767
Publication Date: 1996/11/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Description Models for Concurrent Systems and Their Applications)
Category: 
Keyword: 
stepwise specification,  concurrent system,  topology,  abstract level of description technique,  temporal logic,  

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


Summary: 
We present a topological framework of stepwise specification for concurrent systems in this paper. Some of description techniques can make topologies on the system space. Such topologies corresponds to abstract levels of those description techniques. Using a family of such description techniques, one can specify systems stepwisely. This framework allows to bridge various DTs and modularizing, so that global properties and module properties of systems become to be related to each other. Within this framework, we show derivation of a LOTOS cpecification from temporal logic formulae. An extended version of LOTOS with respect to concurrency is used in this paper. A semantics including concurrency is introduced to do this in this method. The method presented in this paper is applied to mobile telecommunication.