ActLab: an action based toolset (verifying reactive systems by talking to them)

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.