More and more business scenaria involve open systems, i.e., systems composed of interacting entities whose behaviour is not predictable in advance. The complexity 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 automated procedures. A verification procedure will be much more valuable if it is formally proved correct, with respect to the formal semantics of the specification language. Moreover, it is desirable that the system behaviour be tested for compliance against the specification itself, rather than against an error-prone translation. In this article we show how a promising answer to all these requirements could be found in the SCIFF Abductive Logic Programming framework.

A computational logic-based approach to verification of IT systems

CHESANI, FEDERICO;MELLO, PAOLA;MONTALI, MARCO;TORRONI, PAOLO
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 complexity 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 automated procedures. A verification procedure will be much more valuable if it is formally proved correct, with respect to the formal semantics of the specification language. Moreover, it is desirable that the system behaviour be tested for compliance against the specification itself, rather than against an error-prone translation. In this article we show how a promising answer to all these requirements could be found in the SCIFF Abductive Logic Programming framework.
Proceedings of the 14th HP Software University Association Workshop (HP-SUA), Garching/Munich, Germany, July 11-14, 2007.
115
125
M. Alberti; F. Chesani; M. Gavanelli; E. Lamma; P. Mello; M. Montali; S. Storari; P. Torroni
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/45883
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact