Abstract
In this paper 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.
[read the copyright and download the pdf file] [DOI]