PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Mazzanti F., Pugliese R., Tronci E. A Symbolic model checker for ACTL. In: Applied Formal Methods - FM-Trends 98. International Workshop on Current Trends in Applied Formal Methods. Proceedings (Boppard (Germany), October 7-9 1998). Proceedings, vol. 1641 pp. 228 - 242. D. Hutter et al. (eds.). (Lecture Notes in Computer Science). Springer, 1999.
 
 
Abstract
(English)
We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae,and uses symbolic manipulation cilgorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on booleein functions, and by using the BSP interpreter to ccirry out computations (i.e. verifications).
Subject Model ckecking
Formal methods
D.2.4 Software/Program Verification. Formal methods


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional