PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Ristori G. Actlab : verifying reactive systems by talking to them. In: AICA 94 - Congresso annuale (Palermo, Italia, September 21-23 1994). Atti, pp. 1129 - 1144. AICA, 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. Tha AMC checks, in linear time, whether a given LTS satisfies a property expressed by an ACTL formula. The helpful explanation facllity 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 temporal logic formulae easy for the user. Propertlas of raactiva systems are oftan expressed by naturallanguage sentences, thus many impreclslons oceur in the passage tram informai expresslons of system propertles to temporal logie formulae. We thus developed a proto, type translator, NL2ACTL, from Naturallanguage expressions to Temporal Loglc formulae, that would help to generate ! logic formulae, by working aut ambiguitles by maans of interactions with the usar. NL2ACTL has bean intagratad Into ACTlab, providing a way to make tha axprasslon of properties In the logie easier far the user.
Subject ACTLab
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