TPC Workshop Subtopics
Version 1.0
- Relationship with existing industry standards and guidelines used by
certification authorities such as RTCA DO 178C, ISO 26262, ...
- "Packaging" of TP results for submission to
certification authorities, i.e., specific guidance for how
certification authorities should expect verification results obtained
by means of TP should to recorded and delivered as part of the
“certification package”.
- Specific guidance on how certification authorities may decide if a
particular method is a bona fide instance of TP with an adequate
mathematical foundation.
- Specific guidance on how certification
authorities may decide if a particular tool or set of tools that
automate or partially automate TP can be relied upon.
- Specific guidance for the use of TP to verify requirements with
respect to completeness, consistency, traceability (up and
down).
- Specific guidance of the use of TP to verify properties of the
system/software architecture, e.g., temporal and spatial
partitioning. For example, what are the kinds of theorems that
should be proved to verify that a particular application on a platform
can’t modify (or access) the data of another
application.
- Specific guidance that limits the
extent to which assumptions about the environment can be
introduced. (Without such restrictions, the worst case
consequence is the “false implies everything” problem if the
assumptions turn out to be
contradictions).
- Practical uses of TP at the
architecture/detailed design level, i.e., proving that a protocol is
deadlock free or freedom from specific problems such as priority
inversion.
- Specific guidance on the formulation
of verification results for the verification of requirements and the
verification of architectural properties.
- Specific guidance for what should certification authorities expect
when TP is used to verify source code (or other code-like descriptions
of the implementation).
- Specific guidance guidance
about abstractions that are likely to be required to facilitate the
use of TP to reason about code, e.g., an abstraction where the state
of the executing software changes state millisecond by millisecond
when in reality state changes at the GHz rate.
-
Specific guidance about recommended
formulation of verification results for the verification of source
code.
- Specific guidance for how the thoroughness of a set of verification
results obtained by means of TP can be described and what evidence
should be expected by certification authorities. (This is a
non-trivial undertaking if it is to be done with precision that is at
least as good as conventional approach to verification based on
test.)
- Specific guidance for how certification
authorities can be sure about what is meant by a set of verification
results. (Compared to one grand correctness theorem, a set of
hundreds of individual test cases has the advantage that one can
consider each test case one-by-one to understand what has been
verified.)
- Specific guidance for how verification
results obtained by means of TP can be combined with verification
results obtained by means of testing in such a manner that the
possibility of gaps is avoided.
- A "wish list" of example applications of TP that demonstrate specific
elements of the Strawman which are addressed by other subtopics, e.g.,
an example of what should be provided to a certification authority
that a particular approach to TP is sound, or at least, may be relied
upon.
Maintained by Mike Gordon.
This page last updated on Mon Nov 11 2013.