Slides of the HLL tutorial (PDF: 2.57MB)

HLL is a formal declarative and synchronous data flow language in the tradition of Lustre, hence its adequacy to deal with SCADE programs (not limited to). HLL has been developed for certification purposes for RATP and has recently been released as an open-source language. An HLL program follows a cyclic execution: at each cycle, the set of inputs are updated, and outputs are computed according to their data-flow definitions. This synchronous behaviour is standard in control programs that require a highly regulated real-time response to their environment.

HLL is also the main entry point to the PERF workshop used on a daily basis at RATP. The PERF workshop allows a variety of validation and verification activities such as checking the soundness of a specification, proving SCADE programs at low level, proving handwritten source code, proving relay scheme, or demonstrating the equivalence between ADA and SCADE programs or between C and SCADE programs.

During the tutorial, the HLL formal language will be introduced and demonstrated with a number of significant examples, covering the main RATP validation and verification activities. Moreover, a Return of Experience will be provided concerning good practices (modelling, proof), limits and performances obtained. The objectives are to allow participants to understand the approach and to determine if it is suitable for their own validation / verification activities.

A basic knowledge of mathematical logic is required.

Over the past 30 years a major theme within software engineering has been the introduction of Agile Software Development techniques that aim to prioritise responsiveness to change and uncertainty. The pressures that gave rise to Agile are common to all areas of engineering, and attempts have been made to apply the same principles to other engineering disciplines, including systems engineering.

The railway supply chain is increasingly targeting reduced time to market in order to achieve increased competitiveness for high-integrity systems such as traffic management, intelligent trains, etc. Agile development methods are seen as a route to delivering this, but traditionally have not been employed on high-integrity, safety-related rail systems.

In this tutorial Kate will start by considering issues that arise when we apply the principles of agile software development to systems engineering and how Altran has revised the principles to overcome these problems. She will then tackle some key questions facing engineers in the rail domain when called on to implement Agile and the solutions that Altran has developed, including:

• Re-factoring vs up-front architecture: the limits of agile software refactoring in a systems context
• User stories vs formal requirements: capturing the customer need
• Decision management: how to assess and prioritise system decisions while designing for change
• Agile and the safety case: how to manage safety while supporting change, including approaches to engaging with certification authorities and ISAs whose experience may be built on a traditional waterfall lifecycle.

Altran’s high-integrity agile approach combines the best from lean engineering, correctness-by-construction, formal methods, and agile development to find the ‘just right’ blend of disciplines and agility for each project.

Altran has 35 years of experience of delivering safety and business critical systems in multiple domains, including rail, aerospace, and defence. During this time we have developed agile processes for developing high-integrity software products, and adapted the agile principles for application to systems engineering activities.

SafeCap is an approach to formal verification of signalling interlockings that uses static proofs based on first order logic and set theory. Geographic interlocking configuration data is treated as a computer programme and transformed into a transition system. A schema, entered as a pictorial representation of the railway layout, expresses the topological relationships between signalling elements in logical form. In the context of the schema, the SafeCap uses multiple prover tools to automatically verify that specific safety invariants are upheld for each possible step of the transition system. These safety invariants express, in formal notation, the signalling principles that ensure the safety of train movements.

SafeCap ensures fully automated verification in which the input data is read in a standard railway industry format, such as the Solid State Interlocking (SSI) Geographic Data Language (GSL) used in UK railways and all over the world. Diagnostics are expressed in terms typically used by signalling engineers. This makes it easier to integrate SafeCap verification into the existing industrial development processes. SafeCap has proven itself effective in analysing several real-world SSI data sets and identifying errors in such (not in service) datasets. The approach is scalable, it dramatically reduces the rework cycle, decreases the overall cost of development, and improves the quality of signalling.

This tutorial will outline the architecture of the SafeCap toolset, explain how the verification is conducted, discuss our experience in applying SafeCap for verification of large datasets from the UK railway and demonstrate how real-world interlocking data is verified using SafeCap.

Starting with a pre-drawn schema and data set with seeded errors, the attendees will learn how to use the SafeCap tool to automatically identify and correct these errors. They will first learn how to express signalling principles in terms of simple safety invariants that can be proved directly. They will then progress to more complex cases whereby proof of one safety invariant is dependent on proving one or more other invariants.

• More information about the work
• The slides of the RSSR 2019 SafeCap workshop

This tutorial will present the usage of AdaCore’s technology in conjunction with the CENELEC EN 50128:2011 standard. It will describe where the technology fits the best and how it can be used to meet various requirements of the standard.

AdaCore’s technology revolves around programming activities, as well as the closely-related design and verification activities. This is the bottom of the V cycle as defined by section 5.3 in EN 50128.

It is based on the features of the Ada language (highly recommended by table A.15), in particular its 2012 revision, which adds some significant capabilities in terms of specification and verification.

The following tools and technology will then be presented and demonstrated:

• Ada 2012 language
• SPARK 2014 language and verification toolset performing formal proof and verification
• GNAT compiler
• CodePeer - static analysis tool that identifies potential run-time errors
• GNATmetric - metric computation tool
• GNATcheck - coding standard checker
• GNATdashboard - metric integration and management platform
• GNATtest - testing framework generator
• GNATemulator - processor emulator
• GNATcoverage - structural code coverage checker

Those tools will be presented in relation to the design, implementation, testing and integration phases.

In addition, the contributions of the technologies to the Software Quality AssurancePlan will also be shown using tables from annex A – Criteria for the Selection of Techniques and Measures.

The tutorial, using some examples, will be a quick usage guide covering aspects such as boundary value analysis, control flow analysis, data flow analysis, defensive programming, impact analysis and formal methods as referenced in annex D.