A major automobile manufacturer implemented McSCert's improvements to their software development methodologies
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.
McSCert developed automated verification techniques for use in the refurbishment of the shutdown systems for a nuclear power plant
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.
We created a software artifact generation process to improve the very-long-term sustainability and (re)certifiability of software
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.
McSCert provided an industrial partner with customized training in the development and certification of safety-critical software-intensive systems
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.
McSCert works with regulators at a very high level on the challenges of software regulation and certification
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.