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

A circuit approach to LTL model checking

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Niklas Een ; B. Sterin
13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013; Portland, OR; United States; 20 October 2013 through 23 October 2013 p. 53-60. (2013)
[Konferensbidrag, refereegranskat]

This paper presents a method for translating formulas written in assertion languages such as LTL into a monitor circuit suitable for model checking. Unlike the conventional approach, no automata is generated for the property, but instead the monitor is built directly from the property formula through a recursive traversal. This method was first introduced by Pnueli et. al. under the name of Temporal Testers. In this paper, we show the practicality of temporal testers through experimental evaluation, as well as offer a self-contained exposition for how to construct them in manner that meets the requirements of industrial model checking tools. These tools tend to operate on logic circuits with sequential elements, rather than transition relations, which means we only need to consider so called positive testers with no future references. This restriction both simplifies the presentation and allows for more efficient monitors to be generated. In the final part of the paper, we suggest several possible optimizations that can improve the quality of the monitors, and conclude with experimental data.



Denna post skapades 2014-02-27. Senast ändrad 2015-07-06.
CPL Pubid: 194264

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur