Computer Science – Software Engineering
Scientific paper
2010-03-08
EPTCS 20, 2010, pp. 68-75
Computer Science
Software Engineering
Scientific paper
10.4204/EPTCS.20.7
The validation of requirements is a fundamental step in the development process of safety-critical systems. In safety critical applications such as aerospace, avionics and railways, the use of formal methods is of paramount importance both for requirements and for design validation. Nevertheless, while for the verification of the design, many formal techniques have been conceived and applied, the research on formal methods for requirements validation is not yet mature. The main obstacles are that, on the one hand, the correctness of requirements is not formally defined; on the other hand that the formalization and the validation of the requirements usually demands a strong involvement of domain experts. We report on a methodology and a series of techniques that we developed for the formalization and validation of high-level requirements for safety-critical applications. The main ingredients are a very expressive formal language and automatic satisfiability procedures. The language combines first-order, temporal, and hybrid logic. The satisfiability procedures are based on model checking and satisfiability modulo theory. We applied this technology within an industrial project to the validation of railways requirements.
Cimatti Alessandro
Roveri Marco
Susi Angelo
Tonetta Stefano
No associations
LandOfFree
Formalization and Validation of Safety-Critical Requirements does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Formalization and Validation of Safety-Critical Requirements, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formalization and Validation of Safety-Critical Requirements will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-454113