More and more business scenaria involve open systems, i.e., systems composed of interacting entities whose behaviour is not predictable in advance. The complex- ity of such systems increases over time, both in terms of number of interacting entities and of space of possible behaviours. For those open systems whose behaviour is relevant to the business, it is a natural requirement to be able to (i) specify them, and to (ii) verify that the member behaviour in fact complies to the specification. To specify such systems, a language is needed that can cover their possible behaviours, and express the features of such behaviours that are desirable in a given business scenario. The language to be used would benefit from formal semantics, that can identify compliant from non compliant behaviours in a non ambiguous way. The verification of compliance is, in general, performed by means of auto- mated procedures. A verification procedure will be much more valuable if it is formally proved correct, with respect to the formal semantics of the specifica- tion language. Moreover, it is desirable that the system behaviour be tested for compliance against the specification itself, rather than against an error-prone translation.
A computational logic-based approach to verification of IT systems
ALBERTI, Marco;GAVANELLI, Marco;LAMMA, Evelina;STORARI, Sergio;
2007
Abstract
More and more business scenaria involve open systems, i.e., systems composed of interacting entities whose behaviour is not predictable in advance. The complex- ity of such systems increases over time, both in terms of number of interacting entities and of space of possible behaviours. For those open systems whose behaviour is relevant to the business, it is a natural requirement to be able to (i) specify them, and to (ii) verify that the member behaviour in fact complies to the specification. To specify such systems, a language is needed that can cover their possible behaviours, and express the features of such behaviours that are desirable in a given business scenario. The language to be used would benefit from formal semantics, that can identify compliant from non compliant behaviours in a non ambiguous way. The verification of compliance is, in general, performed by means of auto- mated procedures. A verification procedure will be much more valuable if it is formally proved correct, with respect to the formal semantics of the specifica- tion language. Moreover, it is desirable that the system behaviour be tested for compliance against the specification itself, rather than against an error-prone translation.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
