Home Events CSCS Internal Workshop 3
CSCS Internal Workshop 3

 

The third internal workshop of the project Certification of Safety-Critical Software-Intensive Systems was held at McMaster on 28 May 2012, and attended by 20 faculty and graduate students from McMaster and Waterloo.  All presentations were by graduate students or post-doctoral fellows.  The programme was:

 

Defect Localization Using Dynamic Call Tree Mining and Matching.  Anis Yousefi, McMaster.

Abstract:  During testing or maintenance of systems, software engineers frequently encounter programming defects that must be traced and resolved by properly changing the source code. This requires vast understanding of the domain, the code, and specifically of the link between source code constructs and the system’s run time behavior. Defect localization is the process of identifying statements from the source code of a system that are responsible for a failure and is one of the most difficult debugging tasks.

 

In this thesis, we present a novel tool for defect localization, which is able to localize potential defects by looking at the differences between the call tree of a faulty execution and that of a successful one. Using this approach, one will be able to localize defects that change the execution path (i.e., structural defects).

 

The proposed defect localization tool mines frequent patterns from the call trees of passing executions to discover successful paths associated with a certain feature (i.e., functionality) of the system in different situations. It then compares the call tree of a faulty execution with highly relevant patterns to identify suspicious call tree differences. The results can be used as a starting point for further root cause analysis.  slides

 

Validating Requirement Documents.   Chen-Wei Wang,  York.

Abstract:  In this talk we make a first step towards improving an existing standard for the software engineering of safety critical software (CE-1001-STD), issued by Ontario Power Generation (OPG). We propose the format of a precise document of requirements, from which we create a specification consisting of both model contracts and tabular expressions. The specification is made executable by using MSL (model specification library). Having executable specifications means that we can both validate requirements and verify implementations via runtime assertion checking. We also suggest future directions of adopting model checking and theorem proving.  slides

 

A SAT-based Approach to Concurrent Error Detection in FPGA LUTs.   Peter Bergstra, McMaster.

Abstract:  In this presentation we discuss a formal approach to the design of concurrent error detection logic in field-programmable gate arrays (FPGAs). Single event upsets (SEUs) occurring in look-up table (LUT) configuration bits are considered as the fault model. Our approach involves representing the LUT network of the design implemented in the FPGA with constraints to model the presence of SEUs as a boolean formula in conjunctive normal form. It is shown that a satisfiability (SAT) solver can be used to find variable assignments that indicate which circuit outputs can be corrupted by upset events in the specified fault model. An algorithm is presented to automatically generate a parity check code, which will identify with one clock cycle detection latency a malfunction caused by SEUs. The resulting parity check logic can be verified using a SAT solver and it is shown to require fewer LUT resources than duplication for most circuits.  slides

 

IEC 61131-3 Block Library Formalization by Tabular Expressions.   Linna Pang, McMaster.

Abstract:  As a largely used construct in control systems, a Function Block (FB) is an abstraction unit representing component-based systems implemented either by software, hardware, or both. Introduced in the IEC 61131-3 standard, Function Block Diagram (FBD) language is one of five languages for logic or control configuration for a control system such as a Programmable Logic Control (PLC) or a Distributed Control System (DCS). It is important that function blocks are specified and veried formally to ensure correctness. However, we found there is no formal syntax and semantics for function blocks, not even their execution semantics, accepted generally. Formalization can help us detect potential errors of function block based system in early stage of system development.
   

Tabular Expressions, also called tables, are one means to document software requirements and design. They are especially suited to specifying complex relations. Based on this formal model, systems can be precisely specified and verified. For the table to properly define a total function, it is sufficient to satisfy two conditions, disjointness and completeness.


Our research aims at providing formalism and techniques to give formal definitions of function blocks and to address verification issues in the context of safety-critical systems, using tabular expressions. As part of the work, we will formalize a block library that contains commonly used blocks during system design. Annex F of IEC 61131-3 provides a set of basic Program Organization Units (POUs) that we viewed as such a block library. We will formally define this block library by tabular expressions.  slides

 

Time-triggered Program Self-Monitoring.  Johnson Thomas, Waterloo.

Abstract:  Runtime monitoring aims at analyzing the well-being of a system at run time in order to detect errors and steer the system towards a healthy behavior. Such monitoring is a complementary technique to other approaches for ensuring correctness, such as formal verification and testing. In time-triggered runtime monitoring, a monitor runs as a separate process in parallel with an application program under scrutiny and samples the program's state periodically to evaluate a set of properties. Applying this technique in a computing system results in obtaining bounded and predictable overhead. Gaining such characteristics for overhead is highly desirable for designing and engineering time-critical applications, such as safety-critical embedded systems. However, a time-triggered monitor requires certain synchronization features at operating system level and may suffer from various concurrency and synchronization dependencies and overheads as well as possible unreliability of synchronization primitives in a real-time setting. To address these issues, a new method is proposed, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or internal timer. We call this technique time-triggered self-monitoring. An optimization problem is formulated for minimizing the number of points in a program, where self-sampling instrumentation instructions must be inserted. It is seen that this problem is NP-complete. Consequently, a SAT-based solution and a heuristic to cope with the exponential complexity. The experimental results show that a time-triggered self-monitored program performs significantly better than the same program monitored by an external time-triggered monitor.  slides
 

Intersert: Assertions on Process Interaction Sessions.   Augusto Oliveira, Waterloo.

Abstract: Program assertions typically operate on available program state information such as global and local variables. To support sophisticated assert statements such as invariants on inter-process communication, developers must design and maintain supporting infrastructure. Specifically for interaction history, it is non-obvious how to realize this infrastructure: how to maintain the data, how to access it, how to use it in assertions, and how to keep the overhead low enough for embedded systems.

This work demonstrates the utility of assertions on interaction history among system components. It thereby solves the challenges of efficiently maintaining interaction data while
providing an expressive interface for assertions.

Our tool chain enables developers to program assertions on interaction history written in Linear Temporal Logic (LTL).  The LTL statements can incorporate inter-process and inter-thread behaviour. The interaction tracking system incurs a negligible overhead of less than 1%, measured with several benchmarks. This work discusses using LTL assertions and our tool chain with a real-world safety-critical embedded system.  slides

 

A Static Instrumentation Framework for Preserving Extra-functional Properties.  Hany Kashif, Waterloo.

Abstract:  Tracing is a well-established method for debugging software. A developer, either manually or via a tool-chain, instruments a program to trace information such as variable modifications. Current approaches aim only at preserving functional correctness during the instrumentation.  Safety-critical systems, however, are rich in extra-functional requirements such as timing, code sizes, and bandwidth, and thus require new instrumentation techniques that consider also their specific requirements.


In this work, we present the first instrumentation framework that preserves logical correctness and a rich set of extra-functional properties. The framework considers both a developer’s instrumentation intent (II) and automata-based cost models on properties. The proposed framework instruments the input program with respect to the input cost models. It derives instrumentation alternatives based on the II, abstracts the program and prunes the search space, and then instruments the program based on constraints and cost models of competing properties. We demonstrate and experiment with a fully automated framework with different IIs and extra-functional properties. We provide insight into the impact of the various II and cost models on the instrumentation mechanism. slides

 

Recovering and Making Use of the Rationale Behind the CSA N290.14-07 Standard.   Marc Bender, McMaster.

Abstract:  In this talk, I discuss the application of assurance cases to understanding and making use of software standards, in particular the CSA N290.14-07 standard (N290) for qualification of pre-existing software.  After introducing the N290 standard and assurance cases, I will present an assurance case template which represents N290 itself, as well as an assurance case instance which represents the results of an actual qualification activity carried out by our industry partner, SWI.  Lessons learned from the exercise will then be outlined and discussed, critiquing both the standard and assurance cases.  slides

Last Updated on Wednesday, 13 June 2012 13:58