# A Dual-Engine for Early Analysis of Critical Systems

#### Begutachtete Veröffentlichung in Tagungsband

Autor(en):Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich und Mana Taghdiri
In:Workshop on Dependable Software for Critical Infrastructures (DSCI 2011)
Jahr:2011
Preprint/PDF:elghazi-taghdiri-DSCI2010.pdf

## Abstract

This paper presents a framework for modeling, simulating, and checking properties of critical systems based on the Alloy language – a declarative, first-order, relational logic with a built-in transitive closure operator. The paper introduces a new dual-analysis engine that is capable of providing both counterexamples and proofs. Counterexamples are found fully automatically using an SMT solver, which provides a better support for numerical expressions than the existing Alloy Analyzer. Proofs, however, cannot always be found automatically since the Alloy language is undecidable. Our engine offers an economical approach by first trying to prove properties using a fully-automatic, SMT-based analysis, and switches to an interactive theorem prover only if the first attempt fails. This paper also reports on applying our framework to Microsoft's COM standard and the mark-and-sweep garbage collection algorithm.

## BibTeX

@INPROCEEDINGS{elghazi-taghdiri-DSCI2010,
author = {Aboubakr Achraf El Ghazi and Ulrich Geilmann and Mattias Ulbrich and Mana
Taghdiri},
title = {A Dual-Engine for Early Analysis of Critical Systems},
booktitle = {Workshop on Dependable Software for Critical Infrastructures (DSCI 2011)},
year = {2011},
month = aug,
abstract = {This paper presents a framework for modeling, simulating, and checking
properties of critical systems based on the Alloy language -- a declarative,
first-order, relational logic with a built-in transitive closure
operator. The paper introduces a new dual-analysis engine that is
capable of providing both \emph{counterexamples} and \emph{proofs}.
Counterexamples are found fully automatically using an SMT solver,
which provides a better support for numerical expressions than the
existing Alloy Analyzer. Proofs, however, cannot always be found
automatically since the Alloy language is undecidable. Our engine
offers an economical approach by first trying to prove properties
using a fully-automatic, SMT-based analysis, and switches to an interactive
theorem prover only if the first attempt fails. This paper also reports
on applying our framework to Microsoft's COM standard and the mark-and-sweep
garbage collection algorithm.}
}