# A Model-Based Approach to Testing Software for Critical Behavior and Properties

Constance Heitmeyer

► To cite this version:

Constance Heitmeyer. A Model-Based Approach to Testing Software for Critical Behavior and Properties. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. pp.15-15, 10.1007/978-3-642-16573-3_2. hal-01055246

HAL Id: hal-01055246

https://inria.hal.science/hal-01055246

Submitted on 12 Aug 2014

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
A Model-Based Approach to Testing Software
for Critical Behavior and Properties

Constance Heitmeyer

heitmeye@itd.nrl.navy.mil

Naval Research Laboratory

Washington, DC, United States

**Abstract.** To integrate the theoretical concepts of composition and refinement with the engineering notions of software models and components, the Naval Research Laboratory has formulated a set of practical composition-based methods, with associated modeling and proof techniques, for developing critical software systems. The general approach is to develop a set of software components and to use various forms of composition to combine the components in a manner that guarantees properties of the composite system. An assumption underlying this research is that much of the software code can be generated automatically from models using automatic code generators. A problem is that the code generated by such tools still requires testing to ensure that the software delivers its critical services correctly and that the software behavior satisfies critical properties, such as safety properties. The need for testing arises in part because only some of the required code is generated automatically: Stubs are provided for code that cannot be generated automatically (for example, certain algorithms), and such code must be constructed manually. This talk describes model-based methods for developing software, and how the models and properties developed using these methods can be used as the basis for automatically constructing tests for evaluating the correctness of software code. These tests are designed to satisfy various coverage criteria, such as branch coverage. An example is presented showing how our model-based method can be used to construct a suite of tests for evaluating the software code controlling the behavior of an autonomous system.