Careers > Verifying Simulink models with SPARK
Last modified 10/4/2021 9:18:14 AM

Verifying Simulink models with SPARK

Internship
AdaCore
Paris, France or Tallinn, Estonia
Bac + 4/5

Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.

For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.

Our 120 experts worldwide in the US (New York, Lexington), France (Paris, Toulouse, Grenoble and Vannes), the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.

Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.

 

Context:

AdaCore is working on tools to provide the System to Software Integrity (SSI) in the software development process. The aim is to provide a consistent process for refining software specifications from high-level system descriptions to detailed low-level requirements with formal proofs of property preservation. In the context of this work we are experimenting with various methods for formal verification of Simulink models.

 

Goal:

The goals of this internship are to:

  1. Compose simulink models demonstrating typical modelling patterns and contracts, expressed by pre- and postconditions, specifying the model behaviour;

  2. Experiments with proofs of such pre- and postconditions on models converted to SPARK code using the QGen code generator;

  3. Identify successful and unsuccessful modelling and code generation patterns from the provability viewpoint

  4. Suggests ways for reorganization of the code so that proof is possible or easier. 

 

The work includes:

  • Familiarizing yourself with the SPARK language and QGen code generator.

  • Literature reviews and comparisons of existing tools from related work on program and model verification.

  • Developing models for simple algorithms and formal proofs to demonstrate their correctness.

 

Skills required:

  • Good programming skills (C, C++, Java, Python or Ada)

  • Familiarity with formal verification of programs/models.

  • Familiarity with signals and systems and, optionally, control theory

 

Timeframe, location and contacts:

  • 4-6 months - AdaCore R&D department, Tallinn or Paris office

Powered by Hello Talent