PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Ristori G. ActLab : an action based toolset (verifying reactive systems by talking to them). In: ICTL Workshop (Bonn, Germany, June 1994). Proceedings, pp. 68 - 76. Hans Jürgen Ohlbach (ed.). MPI Informatik, 1994.
 
 
Abstract
(English)
In this paper the verification environment ACTLab is presented. ACTLab is centered around the ACTL Model Checker for the branching time action-based temporal logic ACTL. The AMC checks, in linear time, whether a given LTS satisfies a property expressed by an ACTL formula. The helpful explanation facility is available in AMC; also, an interface with the behavioural verification tool AUTO is provided. ACTLab has been designed having a precise purpose in mind: make the specification and the verification of temperal logic formulae easy for the user. Properties of reactive systems are often expressed by natural language sentences, thus many imprecisions occur in the passage from informal expressions of system properties to temporal logic formulae. We thus developed a prototype translator, NL2ACTL, from Natural Language expressions to Temporal Logic formulae, that would help te generate logic formulae, by working out ambiguities by means of interactions with the user. NL2ACTL has been integrated into ACTLab, providing a way to make the expression of properties in the logic easier for the user.
Subject Reactive systems
verification
D.2.4 Software/Program Verification


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