文章基本信息

标题：Verification of State/Event Systems by Quotienting
本地全文：下载
作者：Nicky O. Bodentien ; Jacob Vestergaard ; Jacob Friis 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1999
卷号：6
期号：41
出版社：Aarhus University
摘要：A rather new approach towards compositional verification of concurrent systems is the quotient technique, where components are gradually removed from the concurrent system while transforming the specification accordingly. When the intermediate specifications can be kept small using heuristics for minimization, the state explosion problem is avoided and there are already promising experimental results for systems with an interleaving semantics, including real-time systems. This paper extends the quotienting approach to deal with a synchronous framework in the shape of state/event systems. A state/event system is a concurrent system with a set of interdependent components operating synchronously according to stimuli (input events) provided by an environment while producing output events in return for the environment. A compositional modal logic M suitable for expressing general safety and liveness properties subsystems is introduced. A quotient construction for building components from a state/event system into the specification is presented and heuristics for minimizing formulae are proposed. The techniques are demonstrated on an example. The correctness of the techniques are justified by proofs in an appendix.