TMCnet News
DENSO Using AdaCore's SPARK Technology for Automotive Research ProjectCAR-ELE JAPAN - AdaCore today announced the successful completion of a research project for DENSO, Application of Formal Methods to Help Achieve Freedom from Interference. This project, conducted jointly with the University of Nagasaki, had the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context. The project investigated the use of VDM as a design method, and SPARK as an implementation language, for safety-critical components in systems where legacy C code is prevalent. The SPARK components need to be protected from potential interference from the legacy C code, as required by ISO 26262 ("Freedom from Interference", or "FFI"). DENSO (News - Alert) selected AdaCore because of the company's expertise in formal methods, as proven by the SPARK Pro technology. In the first phase of the project, AdaCore and the University of Nagasaki investigated the FFI problem. The University of Nagasaki team analyzed the use of formal methods and determined that the SPARK approach can significantly simplify the effort in demonstrating system safety. AdaCore showed that the SPARK technology can prove the absence of errors in the critical (high ASIL) components themselves, which simplifies the verification effort. AdaCore also produced guidelines for adding SPARK executable contracts (function pre- and postconditions) to lower ASIL legacy C code. Such contracts can help in demonstrating safety, by insulating the more critical components against failures of less critical components. After the initial phase of the contract was completed, DENSO authorized AdaCore and the University of Nagasaki to continue with Phase 2. During this phase, AdaCore explored the possibility of applying formal methods to the more general problem of safety analysis of a software architecture. The University of Nagasaki used VDM to specify guidelines for applying safety process measures and safety mechanisms to detect / prevent cascading failures. Phase 2 was completed in October 2017. "Our SPARK technology makes formal methods a practical tool for critical automotive software, and we're pleased that DENSO gave us the opportunity to demonstrate these benefits on their FFI project," said J.C. Bernedo, Automotive Market Product Manager at AdaCore. "A frequent question is how formal methods can be used in existing systems where there may be lots of legacy code in C. Our work for DENSO showed that SPARK can be easily integrated and combined with traditional testing-based verification methods, to achieve the highest levels of confidence in the software's reliability, safety and security." "AdaCore is not only a tool vendor but also an excellent research partner," said Mr. Tetsuya Tohdo, Project Manager at DENSO's Tokyo Office in the ePF Advanced R&D Department. "This project gave us a rapid understanding of several research subjects, and we have been able to take avantage of the ideas that were presented. In particular, the proposal for Phase 2 called for the usage of powerful open source tools, and we expect that these will not only promote research projects effectively but will also provide a shortcut to practical applications afterwards. With its technical knowledge of development tools and their underlying research foundations, AdaCore supplied a comprehensive solution." "We use VDM (Vienna Development Method), one of the established model-oriented formal methods for the development of computer-based systems and software," said Professor Shigeru Kusakabe from the University of Nagasaki. "Constructing and analyzing the VDM model helps us to identify incompleteness and ambiguity in the system specifications from the early stages of the development. We are working to combine this well-established formal method with emerging holistic system engineering approaches for FFI."
About Freedom from Interference
About SPARK Pro Using SPARK Pro, developers can formally define and automatically verify software architectural properties, and guarantee a wide range of software integrity properties, such as freedom from run-time errors, enforcement of security policies, and functional correctness (compliance with a formally defined specification). This automated verification is particularly well-suited to applications where software failure is unacceptable. SPARK Pro helps reduce delivery costs and timescales, and, through the use of formal methods, prevents, detects and eliminates defects early in the software lifecycle with mathematics-based assurance. The SPARK language and tools have a proven track record in the most demanding safety-critical and high-security systems.
About AdaCore
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial avionics, automotive, railway, space, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers/ for further information. AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com AdaCore will be co-exhibiting with IT Access Co., Ltd., at CAR-ELE JAPAN, January 17-19, 2018, in Booth E50-18. To request an appointment at the show, please click here.
About DENSO
About University of Nagasaki
View source version on businesswire.com: http://www.businesswire.com/news/home/20180116005413/en/ |