visualSTATE

Verification of large state/event systems using compositionality and dependency analysis A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to significantly improve the efficiency of symbolic model checking of state/event models. It makes possible automated verification of large industrial designs with the use of only modest resources (less than 5 minutes on a standard PC for a model with 1421 concurrent machines). The results of the paper are being implemented in the next version of the commercial tool visualSTATE.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 9 articles , 1 standard article )

Showing results 1 to 9 of 9.
Sorted by year (citations)

  1. Kolchin, A. V.: An automatic method for the dynamic construction of abstractions of states of a formal model (2010)
  2. Jiroveanu, George; Boel, René K.; Bordbar, Behzad: On-line monitoring of large Petri net models under partial observation (2008)
  3. Larsen, Kim G.; Nyman, Ulrik; Wasowski, Andrzej: Modeling software product lines using color-blind transition systems (2007) ioport
  4. Giese, Holger; Vilbig, Alexander: Separation of non-orthogonal concerns in software architecture and design (2006) ioport
  5. Wang, Chao; Bloem, Roderick; Hachtel, Gary D.; Ravi, Kavita; Somenzi, Fabio: Compositional SCC analysis for language emptiness (2006)
  6. Behrmann, G.; Larsen, K. G.; Andersen, H. R.; Hulgaard, H.; Lind-Nielsen, J.: Verification of hierarchical state/Event systems using reusability and compositionality (2002)
  7. Lind-Nielsen, Jørn; Andersen, Henrik Reif; Hulgaard, Henrik; Behrmann, Gerd; Kristoffersen, Kåre; Larsen, Kim G.: Verification of large state/event systems using compositionality and dependency analysis (2001)
  8. Sharygina, Natasha; Browne, James C.; Kurshan, Robert P.: A formal object-oriented analysis for software reliability: design for verification (2001)
  9. Lind-Nielsen, Jørn; Andersen, Henrik Reif: Stepwise CTL model checking of state/event systems (1999)