A formal method to identify deficiencies of functional requirements for product lines of embedded systems

Abstract

Functional requirements that were stated in cooperation with the stakeholders have to be analyzed and reviewed. Deficiencies like incompleteness, contradictions and redundancy within the requirements may lead to an extended development effort. Identifying and resolving these deficiencies in an existing or evolving set of functional requirements for embedded systems is of major importance. Especially, if the requirements describe a set of possible products. Formal methods provide a powerful way to review the requirements automatically. This paper proposes a method adopted from the formal verification of hardware components to uncover the deficiencies within a given set of requirements. The basis of this approach is built by safety properties represented as Linear Temporal Logic (LTL) formulas which are extracted from the requirements. The presented process is evaluated by means of the specification of a car seat.