Michael Weber: Random Bits and Pieces

If we knew what it was we were doing, it would not be called research, would it?

Albert Einstein

New Paper

LTSmin: Distributed and Symbolic Reachability (tool paper accepted for publication to CAV 2010).

Abstract

In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems. These models are typically generated from specifications in high-level languages. The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to archive the resulting labelled transition systems (LTSs), and to minimize them with respect to (branching) bisimulation.

This is a tool paper; a companion technical report provides more details on the methods (its sections on features and benchmarking are by now outdated):
Stefan Blom, Jaco van de Pol and Michael Weber. Bridging the Gap between Enumerative and Symbolic Model Checkers, Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede. (2009)

New Paper

An Embeddable Virtual Machine for State Space Generation, International Journal on Software Tools for Technology Transfer (STTT), DOI: 10.1007/s10009-010-0141-2.

Abstract

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.

(Invited journal version of an earlier SPIN publication.)

We have released version 1.5 of LTSmin. The following improvements have been implemented:

  • New frontend DVE (requires DiVinE-cluster)
  • Bignum support for state counts in spec-reach tools
    (Jeroen Ketema)
  • spec-reach clean-up
  • 'tree' vector set implementation based on AtermDD

The source code, installation instructions and manuals are available online:

http://fmt.cs.utwente.nl/tools/ltsmin/

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.4.

We have released version 1.4 of LTSmin. The following improvements have been implemented:

  • New tool ce-mpi for distributed cycle elimination (Simona Orzan)
  • New tool ltsmin-tracepp for pretty-printing traces to deadlock states
  • TorX support factored out into separate tools {lpo,lps,nips}2torx
  • Enumerative DFS support
  • Enumerative deadlock detection and trace output
  • Reworked ETF support (non-backwards compatible)
  • bash completion for LTSmin tools (see contrib/bash-completion/)

The source code, installation instructions and manuals are available online:

http://fmt.cs.utwente.nl/tools/ltsmin/

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.3.

We have released version 1.3 of LTSmin. The following improvements have been implemented:

  • Regrouping optimizations of the PINS matrix
  • Connection to the CADP toolkit via pins_open
  • Tuning of the BDD usage
  • Significant performance improvements
  • Symbolic deadlock detection and trace output

The source code, installation instructions and manuals are available online:

http://fmt.cs.utwente.nl/tools/ltsmin/

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.2.

Page 1/5: 1 2 3 4 5 »