Balancing Insight and Effort: The Industrial Uptake of Formal Methods - Formal Methods and Hybrid Real-Time Systems - page 244

Test case generation: Where the use of an executable subset enables testing of models,
it can also be valuable to automate the testing process in different ways. Automatic
generation of test cases [59,60] can produce entire test suites [61]. Considering the
balance between effort and insight, this kind of enhancement to the automation of
testing is almost always favourable, particularly when the generated test cases can
be used for testing the final implementation.
Test analysis support: In order to provide further insight into the quality of the test
set used on a model, it is possible to display the coverage of the tests carried out,
for example by using colour in ways similar to those used for programming lan-
guages [62]. Alternatively graphical overviews of executions can be used to give
the user a deeper understanding for what is going on [27]. Depending upon the
time that must be spent creating this kind of feature, it is typically worth the low
effort required to monitor the coverage of tests on a model. The insight into the
functional characteristics of the model is very limited, but it may lead to improved
test sets that themselves prove worthwhile.

3.3 Verification of Formal Models

The expressiveness of formal modelling languages places limits on the extent to which
analyses can be automated. For realistic industrial applications one must normally settle
for as much automation as possible and then provide support for manual analysis [63].
In the area of formal verification one can divide features into those that support formal
refinement and those that support formal proof:

Formal refinement support: Many formal modelling languages have an associated
notion of refinement enabling the description of successively more concrete mod-
els, with a formal relationship between each of them [64]. Many different tools
are able to support this process [65]. Typical approaches involve the definition of
a refinement relation [66,67] between concrete and abstract models. The balance
between effort and insight gained here is problematic from an industrial perspec-
tive unless either there is substantial automation or the correctness of the appli-
cation is sufficiently important to warrant the extra cost in such a fully formal
development [33,68]. However, there is also work towards automated support for
refinement [69].
Theorem provers: The ultimate advantage of using a formal over an informal model
is the ability to verify its properties to a high level of rigour [70], even for infinite
state systems. Given our concern to balance effort and insight, some degree of au-
tomation is required here [71]. A complete reliance on proof automation may lead
to the use of a notation that lacks expressiveness [72]. In reality, for many formal
modelling applications, we would not wish to compromise the accessibility of the
modelling language in order to support a certain level of automated analysis. The
balance between the formalism and the extent of automation is crucial. It depends
on the projects needs: are these to ensure internal consistency by discharging as
many consistency proof obligations as possible, or are they to prove system-level
properties (we have used the term validation conjectures)? In the former case a high