Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2011 - Workshopband P-184, 265-276 (2011).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


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

Florian Markert and Sebastian Oster


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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-278-9

Last changed 04.10.2013 18:35:46