Formal development
Formal Development
Automating code generation of software systems using formal methods.
The process of creating software systems using formal methods.
Automating software development
There is an easier route to rail control
software development
In the endeavor to develop rail control software that meets demands for efficient rail transportation, both now and in the future, many of today’s infrastructure managers find themselves impeded by a number of frustrating roadblocks.
These include long and unpredictable schedules, a general lack of control over systems, and dominant industry issues such as the current oligopoly of system suppliers who deliver systems without consideration for open standards and interfaces.
Formal methods
Formal development to overcome costly barriers in rail control projects
The process used to overcome the common challenges in rail control software projects is Signaling Design Automation. It is a set of automation tools and processes based on formal methods that can be used to develop software for rail control systems.
SDA integrates formal methods
into an automated development process
SDA combines automation with the tools that formal methods offer to ensure that you can efficiently develop rail control systems and verify that they meet requirements during Verification and
Validation (V&V). The automation tools can be used to your advantage at every phase of the software development process – from establishing requirements to system development and maintenance.
Gain more control over your system and quickly identify issues
Capturing requirements for safely testing undefined system configurations is a key concept in the SDA process. This includes a clear separation of different types of requirements (configuration,
interfaces, safety, and test). SDA also promotes the use of open and standardized component formats and interfaces. As a result, you as an infrastructure manager gain more control over your system and acquire the ability to quickly identify and debug
requirement issues before they become a major problem.
How does formal development work?
1. Generation of requirements
Generic requirements for a given type of system are specified and formalized, with a clear separation of design, safety and test requirements. Design, test cases and safety requirements are generated for each application developed.
2. Configuration
The data is split into generic and specific configuration data. From there, you can configure the individual signaling system that you are developing. The tool will take care of creating the specific requirements from your specifications for that particular configuration.
3. Automated verification and validation
The safety requirements are formally verified and test cases simulated. Detailed verification and test reports are generated.
4. Code generation
Code generation tools convert your design into software code to be compiled, configured and installed on the computing platform of the rail control system. This is the software that will be executed on the actual system in the field.
References
Prover’s innovative solutions brings benefits to many types of rail control projects
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
How much can you save by implementing Signaling Design Automation?
In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.
+46 (0)8 617 68 00