Home Events CSCS Internal Workshop 2
CSCS Internal Workshop 2

The second internal workshop of the project Certification of Safety-Critical Software-Intensive Systems was held at McMaster on 16 December 2011, and attended by 25 faculty and graduate students from McMaster and Waterloo.  All presentations were by graduate students or post-doctoral fellows.  The programme (with links to presentations, except two which are commercially confidential) was:


Reducing the risk of patching. Asif Iqbal, Wen Chen, Akbar Abdrakhmanov, McMaster.

Abstract: Large enterprise level systems often have their own application software layer wrapped over large software tool or products from vendors. From time to time, vendors release patches which update or enhance the products to meet various requirements. But applying the patches often introduces risk that the wrapper software layer might behave incorrectly, especially if the customer has little knowledge of it (for example, may be because it is a legacy layer). So there is always the need for reducing this risk. This presentation shows an approach that we are following to reduce such risk for our customer who have their legacy application layer wrapped over Oracle's E-Business Suite and Oracle database. Here we try to find the changes made by the Oracle patches and then trace back to the customer's application layer to find the functions who can potentially be affected by the changes. Thereby we make an attempt to reduce the size of their test suite that they are currently using to find out the risky behaviour, and also to suggest new tests.

Improving bug triaging by combining machine learning and human cognition.  Rafael Lotufo, Waterloo.

Abstract: Software defects—bugs—plague the software development industry, where in average 40-50% of development effort is spent in bug resolution. Suspected bugs are filed in bug reports, which are either fixed, when the fault is confirmed, or closed, when they do not describe a new, significantly severe, fault. To resolve a bug report, the described bug needs to be confirmed, classified with an appropriate severity, and linked to related and similar reports. However, clarity and quality of reports, as well as the non-deterministic nature of bugs, make such diagnosis costly. From the point of view of quality assurance, investigating bugs that will not be fixed is waste of precious developer effort. Triaging teams are employed in most organizations to filter bug reports based on their quality, and to direct the report to the most appropriate developer, that has both the time and capacity to resolve the issue. However, a significant part of triaged reports end up in the hands of wrong developers, much delaying bug fix time. Existing work on automating triaging achieves prediction accuracy of 70%, considering the top 5 predictions. We will present why this is not enough in industry, and our approach to improve such results, combining machine learning with human cognition. slides

Time-Aware Instrumentation with Hardware Support. Hany Kashif, Waterloo.

Abstract: Tracing the execution of embedded systems is particularly important for applications that have non-deterministic behaviour and ones that impose temporal constraints on their execution. Time-Aware Instrumentation allows tracing program execution while honouring temporal constraints. However, instrumentation should still not affect the WCET of a task and thus preventing the instrumentation of basic blocks on the worst-case path of a task. We introduce the notion of conditional instrumentation which allows instrumenting a worst-case path making use of the gap between the estimated and the actual execution times of that path.

State-based Schedules in TrueTime. Akramul Azim, Waterloo.

Abstract: State-Based Scheduling is based on time division multiple access (TDMA) mechanism and supports making on-the-fly decisions at run time. We use Simulink to simulate our patient pulmonary vascular resistance (PVR) monitoring system that uses state-based scheduling. We implement the patient monitor and connect it to a model of a human cardiovascular system using TrueTime. TrueTime supports simulating network communication for real-time control systems. The human cardiovascular system implements a heart model and produces different physiological parameters of the heart. The human cardiovascular system abstracts the implanted body sensors that report PAP, LAP, CO, and PCWP to the external PVR monitoring system. The state-based schedule runs inside the network code machine (NCM) implemented on top of TrueTime. We also used a table tool in the PVR monitoring system for mode changes. slides

Top to Bottom FPGA Formal Verification Frameworks. Honghan Deng, McMaster.

Abstract: Programmable hardware devices are more and more applied in safety critical system such as nuclear power reactor shutdown system. Formal verification is a must for the application of these hardwares in such fields. We applied a top to bottom formal verification framework to prove the netlist after place and route of a FPGA design is correct according to the specification. We use theorem prover PVS to accomplish the design verification and logic equivalence checker as implementation verification to propagate the this correctness to the model in lower level in the design process. In the theorem proof, the formalized implementation model and specification are needed. We can either translate the netlist circuit or the RTL HDL to the formal language in PVS. To facilitate our proof we applied some popular techniques such as hierarchical verification structure and explored some useful techniques such as constrain the model to be more deterministic and introduce signal probes in formal language. slides

Mathscheme.  Russell O'Connor, McMaster.

Abstract: Mathscheme is a project to develop a new approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without sacrificing power or soundness.  In this talk we will describe the framework we are using to achieve these goals, and how Mathscheme can benefit software certification by providing tools for reasoning about specifications and verifying software. slides

Last Updated on Monday, 19 September 2011 17:42