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

PARTIAL UNFOLDING FOR COMPOSITIONAL NONBLOCKING VERIFICATION OF EXTENDED FINITE-STATE MACHINES

PARTIAL UNFOLDING 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)
Göteborg : Chalmers University of Technology, 2013. - 34 s.
[Rapport]

This working paper describes a framework for compositional nonblocking verification of reactive systemsmodelled as extended finite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks in concurrent systems. Compositional verification is shown in previous work to be effective to verify this property for large discrete event systems. Here, these results are applied to extended finite-state machines communicating via shared memory. The model to be verified is composed gradually, simplifying components through abstraction at each step, while conflict equivalence guarantees that the final verification result is the same as it would have been for the non-abstracted model. The working paper concludes with an example showing the potential of compositional verification to achieve substantial state-space reduction.

Nyckelord: Partial unfolding, Extended finite automaton, Verification



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-01-25. Senast ändrad 2016-02-01.
CPL Pubid: 172205

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)

Ämnesområden

Produktion
Datalogi

Chalmers infrastruktur

Ingår i serie

R - Department of Signals and Systems, Chalmers University of Technology