: Testing cycling software components of reactive systems on the basis of formal specifications

Testing cycling software components of reactive systems on the basis of formal specifications

Forschungsergebnisse zur Informatik, Band 40

Hamburg 1999, 169 Seiten
ISBN 978-3-86064-867-4 (Print)

cyclic software, finfite state machines, formal methods, Informatik, predicate logic, reactive systems, testing

Zum Inhalt

Testing is the primary method through which the producer of software and the user or customer gain confidence that the software will work as intended or specified. Using formal methods, which is highly recommended by safety standard and legal requirements in the area of safety-critical embedded software systems, can improve the quality and efficiency of test activities.

In this book, two strategies for testing cyclic software components of reactive systems specified using extended finite state machines (a combination of the specification notations Z and statecharts) are described. A cyclic software component of a reactive system can be viewed as an action that is executed repeatedly, in regular time intervals. During each interval, inputs are read from the environment and, depending on the internal state of the component, outputs are computed. The interaction between function test and trace test is the main concern of the presented strategies. Both strategies are proven to be valid and reliable: They accept any correct program and reject any erroneous one, provided that the test hypotheses are true.



Informationen über das Veröffentlichen wissenschaftlicher Arbeiten.

nach oben