AdaCore Blog

9 entries tagged with #UK

by Yannick Moy

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.

#Formal Verification #SPARK

by Yannick Moy

Rod Chapman on Software Security

Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)

#Security #SPARK

by AdaCore Admin

Certification and Qualification

AdaCore provides several tools with certification and qualification capabilities, for the rail and avionics industry. Quentin Ochem’s presentation on “Certification and Qualification” at the 2015 AdaCore Tech Days in Boston, Massachusetts provided more information about these two standards, namely DO-178C and EN:50128:2011.

#TechDay #Certification #CodePeer

by Yannick Moy, Jamie Ayre, Emma Adby

Ada Lovelace Bicentennial

The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.

by Jack Mellor

2015: A Space Ada‑ssey

AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!

by Jamie Ayre

Verification on Ada code with Static and Dynamic Code Analysis - Webinar

One of the main challenges to get certification in Ada projects is the achievement of 100% code coverage but in most projects an amount of more than 95% structural coverage is hard to achieve. What can you do with the last 5% of code that can't be covered? DO-178C for example, provides a framework for the integration of various techniques in the development process to solve the problem. In this webinar you learn how static analysis and dynamic testing can help complete analysis for pieces of code that are not covered.

#CodePeer #Code Coverage #Dynamic Analysis #Static Analysis #DO-178 #DO-178C

by Martyn Pike

The latest Mixed Programming with Ada lectures at the AdaCore University

I recently joined AdaCore as a Technical Account Manager with an initial focus on the UK and Scandinavian regions, but for the last 12 months I've been busy working on the AdaCore University. The most recent addition to which is a course on Mixed Language Programming with Ada, and it includes lectures on the integration of Ada with C, C++ and Java. The course covers some advanced topics like mixed language object orientation, techniques for using Ada strong typing to combat known issue with C pointers and the pitfalls that are encountered when mixing native Ada code with Java at runtime. This course clearly demonstrates that Ada has strong support for integration with C, C++ and Java and it proves there are no technical barriers to its adoption in modern mixed language software systems.

#Mixed Language #AdaCore University #Java #C++ #C

by Johannes Kanig

Explicit Assumptions in SPARK 2014

In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.

#Formal Verification #SPARK #Testing

by Yannick Moy

Rail, Space, Security: Three Case Studies for SPARK 2014

We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014, in three different domains: rail, space and security. The lessons learned in those three case studies are particularly interesting. Here is the companion paper that we wrote.

#Language #Formal Verification #SPARK