Services

Objectives: 1) to help ensure that the ultimate product is safe and can be certified as such in compliance with relevant medical standards, and 2) to improve the productivity of software developers of focused ultrasound medical devices.

Approach: The research team executed high level hazard analysis using System Theoretic Process Analysis (STPA). We developed a novel approach for assuring safety and effectiveness of complex medical devices which separates the assurance argument into two related, but less complex assurance cases: 1) a Technological Assurance Case (TAC) that presents an argument that the device is safe and effective in terms of its outputs, but does not consider the effect of those outputs on human patients and 2) a Clinical Assurance Case (CAC) that presents the argument that the device is safe and effective for a specific clinical treatment, using information from the TAC.

Result: McSCert constructed an Assurance Case that guides safe and effective development of the system and documents an explicit argument that the Arrayus MRI Guided Focused Ultrasound system is safe and effective. A single TAC can support multiple CACs, each CAC for a different clinical treatment.

Benefit: The project helped Arrayus move closer to Health Canada certification and the eventual marketing of its device. The new safety tools can also benefit Canada’s growing medical device industry, particularly small to medium-sized companies for whom the cost of certification is a tremendous financial burden and risk.

Objective: To develop novel software methods and tools to help ensure the safety of next generation vehicles and to reduce the time and cost associated with software safety activities.

Approach: The research team modeled General Motors’ safety engineering process (SEP) and associated extracts from functional safety standards. We started the project using Goal Structured Notation (GSN) to develop associated safety assurance case templates. We then developed a completely new methodology, WorkFlow+ (WF+), that models the processes and the resulting work products, and helps to generate the safety assurance case.

Result: WF+ is a comprehensive new modelling methodology that is more than a method for generating assurance cases. At its most complete it models the entire SEP and all the work products of the SEP. In this case it provides “complete” traceability throughout the processes, work products and assurance case. It is also useful when employed to (partially) model portions of the SEP.

Benefit: WF+ will help engineers determine which parts of the assurance case can be safely reused and which parts require further engineering effort to ensure the modified system is acceptably safe. The eventual goal is to support incremental design by fully enabling incremental safety assurance.

The project provided training for 25 students, post-doctoral fellows and research engineers in advanced aspects of model-driven engineering, formal methods, requirements engineering and systems safety, including hands-on experience that industrial employers value highly. GM hired five highly qualified engineers who received training through their involvement in the project.

Objective: A large automotive OEM engaged McSCert to help improve their existing software practices.

Approach:  As part of this larger project, one of our graduate students developed a method to systematically simplify mode-switching logic in Matlab’s Stateflow Truth Table blocks through the use of tabular expressions.

Result:  The new methodology has been incorporated into the industrial partner’s production code. At the request of the industrial partner, the graduate student is now applying her method to additional models.

Benefit:  Compared to the original design, the new design is more understandable, easier to test and easier to trace back to requirements.

Objective: To develop a method for the formal verification of function blocks used to program Programmable Logic Controllers frequently employed in safety-critical instrumentation and control systems.

Approach:  McSCert assigned a top PhD student, Linna Pang, to work closely with the power plant and technology consultants, Systemware Innovation Corporation (SWI).

Result:  Pang developed automated theorem-proving techniques and tools to prove the function block designs developed by the power plant’s engineers correctly implement software requirements. McSCert’s tools and techniques met regulatory requirements and were applied by SWI as part of the validation and verification process for the new PLC-based shutdown systems.

Benefit:  The time needed for formal verification was significantly reduced over manual methods previously used. The methods applied by the power plant and SWI engineers were extended to the verification of real-time subsystems. The collaboration provided SWI with the expertise that will make them leaders in an area that is likely to become the standard way of demonstrating dependability of third party software used in safety-critical systems. SWI hired Pang after she graduated.

Objective:  A large power generation company challenged us to improve the very-long-term (25+ year horizon) maintainability and (re)certifiability of software.

Approach:  Our research team executed a radical rethink of the software artifact generation process to better reflect the commonality of knowledge present between artifacts. Software artifacts include, for example, specification documents, design documents, test cases and code.

Result:  We created a generative process that produces most artifacts from a “single source” of the relevant scientific, computing and documentation knowledge. Our generative process gives the software developer and user knowledge and reassurance that all the artifacts actually share the exact same understanding (or misunderstanding) of the task at hand. For future change management and cost-effective recertification, exactly where each part of a piece of code came from is explicitly documented.

More information can be found here.

Benefit:  The artifact generation process automates traceability and makes design choices visible. Human error is removed from the generation and maintenance of documentation, code, test cases and build environments. Overall, the transformative generative process enables significant improvement of the very-long-term sustainability and (re)certifiability of software.

Objective:  Provide advanced training for an industrial partner’s staff working on the refurbishment of the shutdown systems for a nuclear power plant.

Approach:  Informed by our previous collaborative work with the partner and extensive experience in software-based nuclear shutdown systems, we designed and delivered relevant training modules.

Result:  Covering the development and verification of safety critical systems, our training modules represented a formal transfer of Project-developed expertise. The developers and engineers that attended our training sessions are now working on the refurbishment of the nuclear power plant’s shutdown systems.

Benefit:  The McSCert training modules have been used to transfer expertise to further developers and engineers in the nuclear industry and other safety-critical domains. For example, we provided half-day on-site seminar at CANDU on formal verification of function blocks as well as integrated testing and fault injection strategies for FPGAs.

Objective:  Provide technical advice to regulatory and certification bodies striving to develop new guidance to ensure safety-critical software-intensive systems are properly developed and certified.

Approach:  With extensive experience in software certification, McSCert exploits its cross-industry expertise when advising agencies including the US Food and Drug Administration (FDA), the US Nuclear Regulatory Commission (NRC), the US National Institute of Standards and Technology (NIST) and the Canadian Nuclear Safety Commission.

Result:  McSCert recommended the use of Assurance Case Templates to drive development and then to be used for certification. Our recommended approaches incorporate rigorous mathematical reasoning for analyzing the system requirements using tabular expressions and formal methods to ensure consistency.

Benefit:  McSCert’s proposed techniques and methods help industry, regulatory and certification bodies reduce the failures rate of regulated products and processes. Improved and clearer regulatory requirements will result in higher quality products and processes, a reduction in the time to develop higher quality products and processes, as well as a reduction in the time to achieve regulatory approval.