TPC Workshop Subtopics

Version 1.0

Subtopic 1

  1. Relationship with existing industry standards and guidelines used by certification authorities such as RTCA DO 178C, ISO 26262, ...
  2. "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”.

Subtopic 2

  1. Specific guidance on how certification authorities may decide if a particular method is a bona fide instance of TP with an adequate mathematical foundation.
  2. 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.

Subtopic 3

  1. Specific guidance for the use of TP to verify requirements with respect to completeness, consistency, traceability (up and down).
  2. 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.
  3. 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).
  4. 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.
  5. Specific guidance on the formulation of verification results for the verification of requirements and the verification of architectural properties.

Subtopic 4

  1. Specific guidance for what should certification authorities expect when TP is used to verify source code (or other code-like descriptions of the implementation).
  2. 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.
  3. Specific guidance about recommended formulation of verification results for the verification of source code.

Subtopic 5

  1. 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.)
  2. 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.)
  3. 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.

Subtopic 6

  1. 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.