Information Technology Reference
In-Depth Information
we use a subset of the widely known industrial standard PSL from Accellera [1]
and the property checker [13]. A detailed explanation of how the case study has
been model checked using this approach can be found in [29,31].
7
Object Code Verification
In this section we outline our approach for object code verification that is de-
scribed in detail in [30], and we sketch how an associated code verifier can be
formally developed.
7.1
Motivation
Automated object code verification for safety-critical control systems is moti-
vated by the fact that applicable standards for these safety-critical applications,
e.g. for railways [16], require a substantial justification with respect to the con-
sistency between high-level software code and the object code generated by the
applied compilers.
7.2
Approach
The conventional approach for this is
compiler validation
: “Once-and-for-all” it is
validated that the compiler for any input produces object code that is a correct
implementation of that input. However, such an approach is very time-consuming,
especially if it should be done formally (see e.g. [18] for techniques for that), and
furthermore it has to be performed again whenever modifications of the compiler
have been performed. An alternative to compiler validation is
object code valida-
tion
: Each time object code is generated (by an arbitrary compiler), the generated
object code is verified to be a correct implementation of the high-level software
code. Object code verification has the advantage that it is independent of changes
in the compiler and it can be fully automated and reasonably fast, if the compiled
code originates from high-level programs strictly adhering to certain programming
patterns as it is the case for our generated SystemC models.
Our specific approach to object code verification is as follows: To prove that an
assembler program (object code)
A
is a correct implementation of the SystemC
controller model
M
from which it is generated, one should map (see Section 7.5)
A
) given in terms of some
common semantic foundations (I/O-Safe Transition Systems to be explained in
Section 7.3) and then prove that
and
M
to their behavioural models
T
(
A
)and
T
(
M
)areI/Oequivalent(modulo
a variable renaming) by applying transformations that have been proved “once-
and-for-all” to preserve I/O behaviour (see Section 7.4).
T
(
A
)and
T
(
M
7.3
Common Semantic Foundations: I/O-Safe Transitions Systems
In this section we introduce our notion of
I/O-safe transitions systems (IOTS)
and our notion of
I/O equivalence
between IOTS'es.
I/O-safe transitions systems remind about usual transitions diagrams (as de-
fined e.g. in [27]) consisting of (1) a set of variables for which initial values are
Search WWH ::
Custom Search