Workshop: September 5, 13:00-16:00, Volvo Car Corporation
With the rapidly increasing complexity of the mechatronic systems in the automotive industry, it is very hard to reach a sufficient level of test coverage during software testing in different test environments. In near future, it will be almost impossible to only rely on manually generated test cases!
In this workshop, we will present the latest results that have been achieved by integrating new tools and methodologies in the software development chain at Vehicle Propulsion (electric drive, traction battery, charging and combustion engine), in an attempt to assist the test engineers by automatically generating test cases. We will also talk about the next steps in this area. Our ambition is to have a quite interactive session with a lot of questions and discussions. We hope that as many of you can participate from different areas in order to find synergies, exchange information and together drive this area forward.
Relevant target groups include, but are not limited to, software testers, software developers, requirement engineers, technical leaders, and managers.
Seminar September 1, 12:15, EA
Speaker: Angela Wallenburg, Altran, UK
Sometimes software really has to work. SPARK is a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed. By design, the SPARK language is immune to many programming language vulnerabilities (such as those listed by NIST/CWE/SANS). Under the hood, the SPARK static analysis tools use formal verification (automatic mathematical proof).
Generally, formal verification is rarely used in industry due to its high cost and level of skill required. However, over the past 25 years, SPARK has been applied worldwide in a range of industrial applications. A few examples include Rolls Royce Trent (engine control), EuroFighter Typhoon (military aircraft), and NATS iFACTS (air traffic control). Recently, SPARK has been attributed the reason of success for the Vermont Tech CubeSat, the only one of NASA’s 2013 launch of 12 mini satellites (ELaNa project) that remained operational until reentry.
During this talk, you will learn about the rationale of SPARK. We will cover topics such as strong typing, unambiguous semantics, modular verification, contracts, the verifying compiler, scalability, powerful static analysis, combination of test and proof, and cost-competitive development of software to regulations (such as DO-178C).