CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A framework for compositional nonblocking verification of extended finite-state machines

Sahar Mohajerani (Institutionen för signaler och system, Automation) ; Robi Malik ; Martin Fabian (Institutionen för signaler och system, Automation)
Journal of Discrete Event Dynamic Systems (1573-7594). p. 1-52. (2015)
[Artikel, refereegranskad vetenskaplig]

This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.

Nyckelord: Extended finite-state machines, Model checking, Nonblocking, Compositional verification, Supervisory control theory



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-01-27. Senast ändrad 2016-03-30.
CPL Pubid: 231400

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för signaler och system, Automation

Ämnesområden

Produktion
Teoretisk datalogi
Robotteknik och automation

Chalmers infrastruktur