We advocate the need for automated support to System Requirement Analysis in the development of time-and safety-critical computer-based systems. To this end we pursue an approach based on deductive analysis: high-level, real-world entities and notions, such as events, states, finite variability, cause-effect relations, are modeled through the temporal logic TRIO, and the resulting deductive system is implemented by means of the theorem prover PVS. Throughout the paper, the constructs and features of the deductive system are illustrated and validated by applying them to the well-known example of the Generalized Railway Crossing.

Automated deductive requirements analysis of critical systems

GARGANTINI, Angelo Michele;
2001-01-01

Abstract

We advocate the need for automated support to System Requirement Analysis in the development of time-and safety-critical computer-based systems. To this end we pursue an approach based on deductive analysis: high-level, real-world entities and notions, such as events, states, finite variability, cause-effect relations, are modeled through the temporal logic TRIO, and the resulting deductive system is implemented by means of the theorem prover PVS. Throughout the paper, the constructs and features of the deductive system are illustrated and validated by applying them to the well-known example of the Generalized Railway Crossing.
journal article - articolo
2001
Gargantini, Angelo Michele; Morzenti, Angelo
File allegato/i alla scheda:
File Dimensione del file Formato  
p255-gargantini.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 273.38 kB
Formato Adobe PDF
273.38 kB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/75761
Citazioni
  • Scopus 40
  • ???jsp.display-item.citation.isi??? 25
social impact