Modeling-arkiv - Prover - Engineering a Safer World

Prover and Region Stockholm lead model-based approach for traffic control systems

Amanda Öberg — Thu, 03 Jul 2025 09:42:31 +0000

Sweden’s rail and transit systems are facing a generational shift in both technology and expertise. At the same time, the need for more robust, high-capacity, and modern infrastructure has never been greater. To address this, the Public Transport Administration in Region Stockholm and Prover are leading a joint initiative that aims to fundamentally change how traffic control is developed, introduced, and maintained.

Purpose and goals

The main objective of the initiative, called MBATS (Modellbaserat arbetssätt för trafikstyrning/Model-Based Approach for Traffic Control Systems), is to enable a step-by-step digital transformation of traffic control systems by introducing a cross-functional platform and working method based on modeling techniques.

By using digital twins and formal modeling techniques, the aim is to:

improve decision-making through system-wide simulations
increase control over cost, performance, and time during system updates
reduce reliance on outdated, text-based, and manual processes
create a long-term platform for safe and scalable innovation

The approach helps ensure changes can be introduced gradually, without disrupting existing infrastructure or operations. Simulations and scenario analysis enable testing of solutions before deployment, increasing confidence and lowering operational risks.

Long-term effects include:

reduced climate impact through the reuse of existing systems
increased rail network capacity by 20–30% through smarter analysis
shorter lead times and reduced lifecycle costs
enhanced collaboration across departments and suppliers
stronger strategic control of technical assets and investments

The initiative will integrate existing modules and services from the Public Transport Administration’s IT environment to ensure compatibility and scalability. The value to the organization is stipulated through automated services to different users. New work methods are introduced step by step, together with user involvement and recollection of the challenges it entails.

Solution

The core is the introduction of new work methods and a user-friendly environment that enables structured system design, simulation, validation, and continuous improvement throughout the lifecycle of traffic control systems.

The platform supports multiple use cases: from early-stage analysis and investment planning, to operations, maintenance, and future upgrades. A major advantage is the ability to test and verify changes digitally, before they impact passengers or operations.

Background and Prover’s contribution

The innovative builds on the earlier DigiTS project, where Prover and the Public Transport Administration mapped out 20 years of digital transformation across Stockholm’s rail and metro network. The MBATS project is part of the Smart Built Environment program and directly supports its mission to accelerate the digital transformation of the built environment, with a focus on sustainable and interoperable infrastructure.

Prover leads the MBATS project and contributes with its expertise in traffic control systems, digital twin technologies, and formal methods. Prover will deliver several advanced modeling tools and the digital twin platform that is used in the solution.

These tools enable formal, traceable, and repeatable modeling of rail systems. Prover’s solutions help ensure that new configurations meet functional and safety requirements before anything is deployed.

Conclusion

Now, MBATS will integrate digital twins, rail system models, and data flows into a unified digital platform. This model-based approach allows changes to be tested and analyzed before implementation, significantly reducing lead times, costs, and risks while improving safety and system robustness.

By introducing a structured, model-based methodology for traffic control, MBATS lays the groundwork for a smarter, more sustainable, and more reliable transportation infrastructure. The results of the project will be shared with national and international stakeholders and contribute to broader industry learning and innovation.

Timeline and partners

Project start: 2025
Duration: 2 years
Partners: Region Stockholm Public Transport Administration and Prover
Funding program: Smart Built Environment
Key goal: Get in control of existing and future traffic control system

Inlägget Prover and Region Stockholm lead model-based approach for traffic control systems dök först upp på Prover - Engineering a Safer World.

Prover PSL 5.8 released – Now featuring strategy fusion for unmatched performance

Jesper Carlström — Tue, 28 May 2024 13:55:35 +0000

Experience the power of strategy fusion!

Prover PSL 5.8 introduces strategy fusion, a game-changing feature that allows you to fuse multiple model-checking strategies into one (patent pending). No longer will you need to choose between strategies; strategy fusion blends the strengths of each by running them in parallel, letting them tackle assigned problems effectively as a team. And they become stronger together!

For new users: simplicity meets performance

We’ve crafted a powerful default strategy using Strategy Fusion, perfect for those new to Prover PSL. You don’t need to be an expert in strategy craftsmanship to get started. Simply run Prover PSL without specifying any strategy, and the default will handle most tasks with ease.

For experienced users: enhanced performance

Seasoned users will notice significant performance boosts in both SAT solving and advanced model checking. Prover PSL continues to deliver the best model-checking performance on the market.

Upgrade to Prover PSL 5.8 today and experience model checking with strategy fusion!

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Prover PSL 5.8 released – Now featuring strategy fusion for unmatched performance dök först upp på Prover - Engineering a Safer World.

Why every rail control project should start with a digital twin

Anders Linden — Tue, 22 Aug 2023 09:57:18 +0000

When you’re tasked with the mission of procuring a new rail control solution, taking time to clearly specify your needs, requirements, and expectations is a critical first step.

Doing so helps you avoid common project roadblocks— like long and unpredictable delivery schedules, tender specification issues, or errors discovered too late in the production process. It also gives suppliers a fair chance to develop the system they need in a time and cost-efficient manner. Furthermore, having clear specifications makes it easier, for infrastructure managers, to evaluate with accuracy how well systems comply with quality, safety, and other important requirements.

However producing specifications can be a challenge in itself. How can you be certain that your specifications actually correspond to your needs? Or that they will be interpreted correctly by all stakeholders? Our recommendation is to take a formal approach to develop a prototype, or a digital twin, that you can use to validate your specifications with simulation and formal verification.

What is a digital twin?

A digital twin is a virtual, interactive replica of an actual physical system, asset, or process. Applied to the railway sector, a digital twin could cover the entire infrastructure – from stations, rolling stock, switches, and signals to supporting IT systems.

It helps infrastructure managers to formulate and evaluate precise requirements for their system, and to ensure that these requirements are verifiable. The result will be precise and clear test and safety specifications for the supplier to deliver against.

Suppliers can then use the digital twin as input for the detailed design, using automation tools for code generation, testing, and verification, further shortening project schedules and reducing costs. The digital twin will be used throughout the lifecycle of the system, reducing costs related to upgrades and adding new features during the maintenance phase.

Ensure you get the system you need at the best price

There are multiple benefits to starting off your next rail control project with a digital twin. With help from automation and stronger verification and validation tools, you reduce risks and resource needs while, ultimately, allowing high-quality software to be delivered in a more predictable way.

Main benefits of a Digital Twin:

Simplifies rail control solution procurement processes
Enables an efficient validation and verification process
Reduces the risk of misunderstandings and project delays
Allows for more predictable delivery schedules and costs
Shortens the time needed for costly on-site tests
Minimizes the risk of error discovery late in the procurement process
Makes it easier to accurately gauge if systems comply with requirements

How to create a digital twin?

When creating a digital twin, the first step is to specify the requirements for the function and safety of the system, these are then used to define the design specification for the implementation. An object model is also defined, serving as a common interface for the test, safety, and design specifications, so that these can be developed independently. This is done using an iterative, test-driven, and agile process consisting of the following steps:

1. Gather and analyze input
The process starts with an analysis of the needs and available information to define the test and safety requirements on a high level. Tender requirements, use cases, legacy systems, applicable standards, interfaces, rules, regulations, and project scope provide input to this task.

2. Formulate requirements and define the object model
Formulate the test and safety requirements in natural language using an object model that defines the objects in the system and how they interact. The test and safety specifications are then used to define the design specification, for the implementation of the system. The specifications are refined and validated later on in the process.

3. Configure your digital twin
Specify the configuration data that will be used to create instances, or specific applications, of the object model.

4. Validate the design, test, and safety requirements
Define, or implement, the object model and requirements in a formal language that can be used to automatically generate a model for a given system configuration. Validate the requirements with automated simulation-based testing and formal safety verification, using the digital twin configuration. This process will reveal, and help resolve, any ambiguities and missing precision in the formulated requirements.

Learn more about how digital twins can help your railway development project.
Book a meeting with us.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Why every rail control project should start with a digital twin dök först upp på Prover - Engineering a Safer World.

The key to a successful rail control project

Anders Linden — Mon, 03 Jul 2023 07:30:54 +0000

Despite exciting technological advancements, carrying out a successful rail control project today remains a complex burden with a multitude of challenges for both infrastructure managers and suppliers. Here, we’ll take a deeper look at the underlying issues and discuss how implementing Signal Design Automation can help you eliminate inefficiencies and costly errors—and finally gain control over your systems.

What’s standing in the way of your successful rail control project?

There are a number of factors standing in the way of a successful rail control project. Rail control systems are expensive to procure, develop, and maintain. Costs and schedules are routinely exceeded. Errors and shortcomings in procured systems are often discovered late when it’s too difficult to make changes. And attempting to address all these problems causes further delays to the entire process before systems can finally be put into revenue services. All in all, this generates a lot of frustration for all parties involved and contributes to the end customer feeling out of control.

Underlying these challenges is the fact that the railway market is still relatively conservative when it comes to adopting future production processes that are related to these systems. And the relatively small number of dominant suppliers in the market today makes driving the change that’s needed even more difficult.

Common challenges in rail control projects

Systems are costly to procure, develop, and maintain
Costs and schedules are routinely exceeded
Proprietary solutions, reducing competition and creating vendor lock-in
Errors and omissions are discovered late
End customer not in control
Conservative attitude to future production processes (slow and inefficient production)
Supplier landscape “oligopoly” (few dominant suppliers)
Status quo being preserved

Rail control project stakeholders

In rail control projects, the main stakeholders are the Infrastructure Managers (IM), who own the rail control systems, and the Suppliers who develop these systems. There are also a number of system consultants and vendors involved.

Addressing the root causes

By digging down to the root of the common challenges in rail control projects, we can more easily identify what kinds of solutions are needed in order to move past them. There are three main root causes that need to be addressed.

Root cause #1: Tender requirements tend to be imprecise
The first root cause is related to what the customer actually needs. Tender requirements for rail control systems tend to be imprecise, with a lack of clarity regarding what the requirements actually are for the system standard. This can lead to suboptimal design choices, with drawbacks that might not be discovered until it’s too late and too expensive to make changes. It can also lead to a system being delivered based on proprietary choices, resulting in vendor lock-in.

Root cause #2: Verifications are based on traditional methods
Another root cause is the fact that the verification activities, which are used during development and before commissioning, are very much based on outdated methods. For instance, the time-consuming and error-prone review and testing processes. While reviews and testing are useful and important, the verification coverage is poor. That is, you can detect the issues but you cannot prove that there are no issues remaining. So, together with the first root cause, vague and imprecise requirements make it really difficult to perform verifications well because relying only on human judgement usually causes a bottleneck.

Root cause #3: Lack of standard architecture and interfaces
The third root cause is a lack of standard architecture and interfaces. Of course, standards and standard interfaces do exist, but when it comes to the actual systems, there are many parts of those systems or subsystems that don’t really belong to a standard architecture or have standard interfaces. This makes it a little more difficult to reuse requirements and know-how about systems. And if you have multiple suppliers, you may have to duplicate the effort for each system. This also makes it harder to use commercial, off-the-shelf components and prevents you from going as far as you may want to when it comes to plug-and-play concepts.

Our solution: Signaling Design Automation (SDA)

All of the challenges infrastructure managers and suppliers run up against during rail control projects can be solved by adopting a better production process. At Prover, our mission is to supply the industry with tools and processes that meet the requirements and expectations of the end customers. We do this by focusing on the requirement specifications, using automation to develop the systems, and applying formal and automated methods to prove that the requirements are fulfilled.

So what does a better production process look like? Our solution is something we call Signaling Design Automation (SDA).

What is SDA?

SDA is a set of automation tools and processes, based on generic, formal specification principles, that is used to develop the software for rail control projects. The idea is that SDA instantiates these generic principles for a particular configuration and produces the design and software code for a particular system. SDA also performs safety verification to produce safety evidence, as well as automated testing to create a test report. These point tools are highly automated and based on the principles, the configuration, and the actual code. Of course, it’s also possible to use different code generation back-ends to generate the code.

4 steps to a successful rail control project

Here is a summary of the actions needed to address the most common challenges and, finally, run a successful rail control project using SDA.

1. Structure your configuration data and system requirements
The key to success in any rail control project is creating a proper specification of the project’s needs, requirements, and expectations. The infrastructure manager needs to specify their own knowledge of both the solutions that they already have and of the solutions that they want to be delivered in the future.

2. Create a Digital Twin before tender
With this in mind, infrastructure managers can do a better job with tender specifications. Creating a Digital Twin before a tender is made is a practical way to get to a point where requirements are more precise and systems can be verified. Of course, this is also a critical action when it comes to procuring systems at a reasonable price, because it gives suppliers a better chance of meeting expectations

3. Use SDA tools to improve approval-related V&V
Both infrastructure managers and suppliers can use SDA tools to improve the verification and validation (V&V) that needs to take place before software systems can be approved for revenue service. This can include both simulation (standard test suites) and formal verification (verifying requirements on configuration data and safety as well as testing). This also gives improved coverage in V&V and reduces the effort and time required for safety assessment. Especially if you replace more traditional approaches.

4. Use SDA to deliver software based on the Digital Twin
Finally, SDA can be used in its full context to develop and deliver software based on the Digital Twin. This is a way to adopt future production processes, including more automation and stronger V&V tools, and—as a result— reduce risks and resource needs, and allow high-quality software to be delivered in a more predictable way.

Learn more about how Signaling Design Automation can help you run a more successful railway development project here.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget The key to a successful rail control project dök först upp på Prover - Engineering a Safer World.

If the railway was invented today, how would we manage our systems?

Mats Boman — Tue, 09 May 2023 06:35:21 +0000

Imagine that today is the day that the world is inventing the railway, and you are part of the steering committee. With access to all of the technology that this modern age has to offer, how would you choose to manage the systems, and which methods and solutions would you use?

There are some easy answers to these questions. But do we approach our current systems like this? Of course we don’t. We are stuck with existing technology, organizations and businesses. We will never be able to use the latest technology nor the most innovative solutions. There is an (un)natural process with many obstacles to overcome before a new technology can be introduced. Many obstacles can be traced back to man’s inability to adapt to new technology, adding the complexity of doing so in a safety environment, which the railway is. There are multitudes of guides and standards to address before you are allowed to use new technology in the rail context, many based on history which you need to respect.

But, for a moment, let us not consider those obstacles. Instead, let us ask, how would we like our rail system to be built and maintained today? And what, from this, can we adapt to in our current reality?

This blogpost is more about methods and solutions for managing and developing our systems than the actual devices or products they would use. Why? Because technology will change over time, and designing a system that is independent of the actual technology is key to making our rail solutions work for a long time.

Why do we need a railway system in the first place?

In other words, is this the transportation system we will have for all time? Possibly not. What will the value of transporting people and goods in “connected boxes” on rails be in the future? (Again, let us not get stuck with technological solutions.)

What we are trying to achieve in our railway systems is the safe transportation of people and goods on rails with specific conditions, such as low resistance between metal rails and metal wheels. Low resistance actually forms the basis of the business case for the very existence of railways; low energy consumption gives a better climate, higher speed, etc.

How hard can it be to safely move boxes on a predefined network of tracks? This is the solution we need to invent, and it’s not the hardest case for any engineer today. The ease of the challenge, or the underestimation and disrespect of the complexity in signaling, is actually one of the biggest hurdles to overcome when managing the introduction of a signaling system in a project. With or without knowledge, unknown challenges and uncertainties will arise that need to be managed. (Many of such hurdles arise from history, which are discussed in another blogpost that you can read here.)

Now, back to the solution.

Of course, if given the chance, engineers would use modeling and AI to support the innovation of a railway system. They would structure the innovation utilizing best practices from a system engineering perspective and use tool support. They would use several models to understand the innovation. Labs would be built to manage and evaluate the technical solutions. Real tracks, vehicles or products would be used only after all other possible means of analyzing and guaranteeing their function have been used. And, if we also include the maintainability and upgradability aspect, all operations would be logged and recycled back to all parts of the innovation.

This process, the system life cycle, would be automated with the generation of new versions that could be evaluated and controlled before being taken into revenue service. We would be in full control of all modules, communications, behaviors and interactions,both in operation and in digital form. We would have capabilities to evaluate and introduce new technology over time.

So, how far away are we from such a system? And where do we start?

Many of the steps that need to be taken to make this system a reality would involve accepting the challenge and acknowledging the complexity in today’s system. First, we need to be in control of our current system and its life cycle. One way to get there is to digitize our system data, create digital models and automate our processes.

Digitization is initially an uphill battle with upfront costs and payback later on. We can sometimes argue for direct effects from digitalization, but the greater return of investment will come in the future. Still, it is necessary in order to understand current relations between subsystems and to remove obstacles before introducing new system technology. At the same time, it could be done stepwise, system by system, with the acceptance that we will gradually upgrade our knowledge and will not realize the full effects until later—with the introduction of a new subsystem, technology or easier maintenance.

Digitization is initially a cost that pays off over time, if the digital system is introduced with the aim of developing over time.

Process automation is the key to being able to maintain the digital representation of our evolving system

When we are in control, we can actually start to simplify and become more efficient. Today’s systems are, in many ways, overly complicated by regulations (because we do not dare to remove anything from a safety system). Regulations are usually the last thing to change. Having extensive experience with a given technology and methods is one way to guarantee safety but, at the same time, it poses a barrier to innovation. Regulations should be focused on the end product in its own context, with qualitative requirements and quantitative measurements that are formalized–not as it is today, where the focus is on the development process which, contentiously, will evolve.

As a researcher, at KTH the department of Engineering Design, complexity and uncertainties once taught me, “complexity is not managed by adding requirements nor processes. It is managed by awareness and competences that continuously work to reduce the complexity.”

Being in control and continuously working with a system on all levels will create a sustainable system that is up to date. Knowledge will be kept by the system model, and system managers should direct resources towards means of improvement, not just towards keeping the system alive.

These principles mirror the ideas and background behind the development of digital twin technology, which you can read more about here.

About the author

Mats Boman has been working in the railway industry since 1999. His career started at Prover and, after switching gears to drive a consulting business within rail control system management and then serve as the CEO of the rail engineering company STHK, he recently returned to Prover as the Vice President of Business Development. Mats has a master’s degree in computer science from Uppsala University.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget If the railway was invented today, how would we manage our systems? dök först upp på Prover - Engineering a Safer World.

Case: Developing digital twins for the Stockholm Metro

Gunnar Smith — Mon, 11 Jul 2022 07:56:05 +0000

When the Stockholm Metro set out to upgrade their rail control system, they contacted us at Prover to assist with the transition.

Stockholm Metro’s system consists of a central traffic management system and a relay-based vital and non-vital signaling system distributed over several relay rooms. The plan is to replace the mechanical control panels used by the operators with a modern computerized traffic management system, as well as to replace the non-vital relays with a distributed PLC solution, and, at least for the time being, leave the vital relays intact.

In order to analyze the existing systems and validate this approach, a digital twin of the system was developed using formal methods. These formal methods included formal specifications with an emphasis on the interface, separation of configuration data and generic requirements, automated simulation-based testing, and formal safety verifications.

CLIENT: Stockholm Metro
LOCATION: Stockholm, Sweden
DATE: 2021-2022

Project goals

In this case, the Stockholm metro had three primary goals. The first was to discover any dependencies that would make it difficult to leave the vital relays untouched.The second was to identify any safety critical functions that are dependent on the existing non-vital relay or control panel design, to include such requirements in the specifications for the new systems. For example, physical wiring may prevent certain commands from being received simultaneously, or safety standards and best practices may have changed since the original system was commissioned. And finally, they wished to test out the concept in order to avoid any surprises that could delay the project and make it more expensive.

PROJECT START

At the start of this project, the Stockholm Metro’s architecture consisted of the following components:

Physical maneuver panel – Push/pull buttons and switches for controls, lamps for indications
Non-vital relays – Interface between panel and interlocking, with additional (non-safety related) logic

Vital relays – Safety related signaling logic, locking of routes and points, signal aspects

END GOAL

The end goal of the project was a future architecture consisting of:

A computerized traffic management system with an operator interface
A set of PLCs with the same functionality as the current non-vital relays
The vital relays from the original system left intact, interfacing with the PLCs

The solution in 6 steps

Created a digital twin of existing system
Carried out formal verification of the safety of the current system
Automatically generated the PLC application software
Created a digital twin of the future system
Replaced the model of the PLC with an actual PLC
Replaced the model of the interlocking with the actual relay system

Results

Following this process, the Stockholm Metro was able to successfully validate the modularity of the proposed system and establish that it is feasible to replace the non-vital relays with a PLC system. They were also able to identify a few unexpected details in the existing system.

Furthermore, the digital twin validation approach simplified the transition to the physical environment relay system–testing with the PLC installed in the field was conducted over the course of a single night.

In the future, the Stockholm Metro can use the digital twin for preparing tenders, validation and verification, reproducing issues from field error reports/logs, replacing testing in the field, and training and documentation.

Inlägget Case: Developing digital twins for the Stockholm Metro dök först upp på Prover - Engineering a Safer World.

The need for digital twins in rail control projects

Gunnar Smith — Tue, 01 Feb 2022 12:17:50 +0000

When it comes to unlocking future growth in the rail sector and beyond, advancing digital transformation is high on the European Union’s agenda. One of the keys to making this happen is the uptake of new fundamental technologies such as digital twins. Here, we’ll discuss the benefits of digital twins in rail control projects, and how the technology fits into our signaling design automation process to help infrastructure managers carry out more successful rail control projects.

How digital twins benefit the rail sector

A digital twin is essentially a virtual, interactive replica of a real physical system, asset or process, including its real-time characteristics and behaviors. Applied to the railway sector, a digital twin encompasses the entire infrastructure—from stations and signals, to the coordinating IT systems.

Infrastructure managers as well as remote repair crews and station staff stand to benefit from having a digital twin of a railway. With access to a real-time 3D representation of the entire railway infrastructure, maintenance and repairs can be performed faster, and more proactive decisions can be made to prevent safety hazards and costly mistakes, while improving overall efficiency.

But the digital twin is also immensely beneficial when put to use early on, before a railway’s subsystem has even been specified, to ensure the right system is built in the first place.

Using digital twins to develop better rail control systems

Creating a digital twin at the start of a rail control project, before tendering begins, enables infrastructure managers to formulate and evaluate more precise system requirements and—ultimately—procure better systems at a more reasonable price.

At Prover, a digital twin is developed using formal methods that utilizes automated simulation and formal verification.

Suppliers can use the digital twin as input for the detailed design, using automation tools for code generation, testing and verification, and further shortening project schedules and reducing costs. The digital twin can then be used throughout the lifecycle of the rail control system, reducing costs related to upgrades and adding new features during the maintenance phase.

Digital twins implementation

Simplified rail control solution procurement processes
More efficient validation and verification process
Reduced risk of misunderstandings and project delays
More predictable delivery schedules and costs
Less time needed for costly on-site tests
Minimizes the risk of error discovery late in the procurement process
Makes it easier to accurately gauge if systems comply with requirements

Learn more about how digital twins can help your railway development project.

Book a meeting with us.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget The need for digital twins in rail control projects dök först upp på Prover - Engineering a Safer World.

Using HLL to solve Sudoku puzzles

Lars Helander — Wed, 10 Jul 2019 09:37:45 +0000

In a recent post we celebrated the 10th anniversary of the declarative, formal language HLL. The language is used extensively in the railway signaling domain for the formal verification of interlocking logic and CBTC subsystems (such as zone controllers). In this more technical post we will familiarize the reader further with HLL, by formalizing the famous Sudoku problem in the language, and using an off-the-shelf proof engine to solve Sudoku puzzles.

The Sudoku problem is a very easy problem for modern proof engines (such as SAT solvers), but it will serve us well in introducing the reader to HLL. To be sure, we will only be able to illustrate a relatively small subset of HLL, a language which has grown quite a bit over the years. To formalize and solve Sudoku problems we will mainly need integers, arrays and quantifiers.

Creating the grid

We start by representing a partially filled Sudoku grid using a 9×9 matrix where each element is an integer in the range 0 to 9. Empty slots are filled with zeroes. The problem itself was in the "Very Difficult" category over at 7sudoku.

Declarations:
 int partialGrid[9][9];
Definitions:
 partialGrid := ;

Then, we will define our problem grid by replacing the zeroes in the partial grid with unknown integers in the range 1 to 9. Creating unknown (or free) variables in HLL is very simple: we just need to declare them.

Declarations:
 int [1,9] unknown[9][9];
 int [1,9] grid[9][9];
Definitions:
 grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] 
                                         else partialGrid[i][j];

Expressing the Sudoku problem

Now, we will express the Sudoku problem itself over our grid, by using quantification. Remember that the objective of a Sudoku is to fill the grid so that all rows, all columns and all of the nine 3×3 subgrids each contains all the digits from 1 to 9. In HLL, array-indexing is 0-based, yielding the below formulation of our Sudoku-objective.

Definitions:
 objective := ALL digit:[1,9] (
    ALL row:[0,8] SOME col:[0,8] (grid[row][col] == digit)
  & ALL col:[0,8] SOME row:[0,8] (grid[row][col] == digit)
  & ALL subgridRow:[0,2], subgridCol:[0,2]
      SOME sRow:[0,2], sCol:[0,2]
    (grid[subgridRow * 3 + sRow]
         [subgridCol * 3 + sCol] == digit));

Finally, we will ask a proof engine whether our objective is attainable (or satisfiable) or not. We do that by trying to prove that there is no solution (by negating the problem). If there is a solution (i.e. a counterexample to our proof), the proof engine will provide us with it.

Proof Obligations:
 ~objective;

Using a modern proof engine (such as Prover SL Certifier Edition) we will be provided with a solution in a fraction of a second.

$1*: grid[0][0] is [1]
$2: grid[0][1] is [7]
$3: grid[0][2] is [6]
$4: grid[0][3] is [4]
$5: grid[0][4] is [5]
$6: grid[0][5] is [3]
$7: grid[0][6] is [8]
$8: grid[0][7] is [9]
$9: grid[0][8] is [2]
    ...
$80: grid[8][7] is [2]
$81: grid[8][8] is [9]

Improving the presentation

To improve the presentation a bit, we will use the temporal dimension of HLL (cf. LTL). HLL is a language based on streams, which are just infinite sequences of values, one for each discrete time step. The idea is to transform the 9×9 grid into 9 streams (representing the rows), of which we will inspect only the 9 first values. Doing this is a bit technical. We need to 1) redefine the grid as a memory that keeps its value in each time step, and 2) define a counter that counts time steps modulo 9 (starting at 0), before we can create our 9 "stream rows".

Declarations:
 int [0,8] counter;
 int [1,9] rows[9];
Definitions:
 grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] 
                                         else partialGrid[i][j],
               grid[i][j]; // Keep value in next time step
 counter := 0, (counter + 1) % 9;
 rows[i] := grid[i][counter];

Finally, when asked to extend the solution up to the 9th time step, the proof engine provides us with a prettier view of the Sudoku-solution (without any measurable time penalty by the way).

$1*: rows[0] is 1 7 6 4 5 3 8 9 [2]
$2: rows[1] is 9 4 2 7 8 1 3 6 [5]
$3: rows[2] is 5 8 3 6 2 9 7 4 [1]
$4: rows[3] is 3 9 1 5 4 6 2 8 [7]
$5: rows[4] is 6 2 7 9 1 8 5 3 [4]
$6: rows[5] is 4 5 8 2 3 7 9 1 [6]
$7: rows[6] is 2 1 4 8 9 5 6 7 [3]
$8: rows[7] is 7 3 9 1 6 2 4 5 [8]
$9: rows[8] is 8 6 5 3 7 4 1 2 [9]

Note that this is the raw, unedited, output given by the proof engine's "Why"-module, which can be used to interactively explore counterexamples.

Summary

To summarize, we have shown how the well-known Sudoku problem can be formalized in HLL and solved using a general purpose proof engine (don't hesitate to contact sales@prover.com to buy your own license!). The output has been optimized using prefixes of length 9 of streams (sequences of values), so that it looks almost like what one would expect from a purpose-built Sudoku solver.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Using HLL to solve Sudoku puzzles dök först upp på Prover - Engineering a Safer World.

Challenges in digitizing specific application configurations

Olav Bandmann — Tue, 04 Sep 2018 08:49:24 +0000

To enjoy the full benefits of Signaling Design Automation, particular care needs to be taken regarding the Specific Application Configuration.

Characteristics of specific application configuration

Specific Application Configuration (SAC) often involves large amounts of safety critical data organized in an inhomogeneous fashion. Data might be given as scheme plans, control tables, and/or in written documents, notes, etc. In some cases, the data is only communicated verbally or is even implicit as a common understanding among involved engineers.

The typical configuration process therefore tends to be error prone and time consuming. This also applies to any independent checking and verification of the final configuration. Over time, maintenance also becomes even more difficult.

Weakly and partially specified configuration data distributed over many types of sources is not an ideal way for an efficient and reliable process.

A way forward?

A way forward is to have a well specified set of SAC data organized in a uniform way in a “human friendly” open format. Such a format would also make it possible to use tool support for performing trusted computations on the SAC data for checking static requirements and for producing derived data.

In a generic approach this requires a Generic Application Configuration (GAC) containing the specification of the SAC data. The GAC is a natural place for specifying static checks and derived data.

Geographical data would preferably be represented in some compact easily reviewable format, and there should be support for tabular data.

The layout configuration format – A uniformapproach

The Layout Configuration Format (LCF) and its supporting tools released by Prover address these problems. It realizes a CENELEC SIL-4 compliant process that gives:

a general and consistent way to represent all required SAC data for any given interlocking in a compact and review friendly file format
a generic way to specify which SAC data is required and how it should be used for any given interlocking type
an interface that is used to document how to collect and interpret the various pieces of data that make up the configuration of the specific application, in order to map it to LCF
a method to configure algorithms to compute derived SAC data from given SAC data in a trusted way, in order to minimize the amount of data to create and review
a highly configurable method for transforming SAC data to standardized tables and variable mappings for code generation and sign-off verification
a format with accompanying tools that are independent of signaling principles, design tools, and interlocking platform.

Find out more about LCF here.

Inlägget Challenges in digitizing specific application configurations dök först upp på Prover - Engineering a Safer World.

How to write a decent spec

Daniel Fredholm — Tue, 27 Mar 2018 09:38:31 +0000

Anyone who has given it a go knows that writing specifications is hard work. In fact, at times it seems almost impossible. Which probably is the reason why the practice of using specifications is shunned and dodged whenever possible. Which is bad.

However, if one finds oneself working in the field of railway interlockings, they cannot be avoided. Which is good. So why is it hard to write a good one? And how do you do it?

To me, the main difficulty in writing a good specification is choosing an appropriate level of detail. Let me explain what I mean with this. Software development is a journey from fluffy abstract ideas (‘it should be safe’) to gritty concrete code (‘ExtIsRed := if …’), with the ambition that some of that fluffyness is actually captured in the final code; not an easy task. The fact that the person with the fluffy abstract ideas is usually not the same as the one who writes the code does in no way make this easier. In fact, these persons serve very different purposes in the development process, one making demands and the other one implementing a software product that has to meet these demands. This is where the specification enters the picture. The specification serves as the bridge, or the interface, between the two.

At this stage, perhaps the point I was trying to make becomes a bit clearer. Since the specification serves as a bridge between the user and the implementer, it has to fulfill two purposes; it has to be understood by two parties, and those parties can be quite different sorts of characters regarding education, skills, ways of expression and even personalities. The specification should be detailed enough so that demands and requirements are expressed in a clear and understandable way, but also not too detailed in order to leave some space of manoeuvring to the implementer.

If it is so hard writing good specifications, is it even worth trying? the reader may ask. Well, if one has any ambition at all concerning user satisfaction, or following safety regulations, then the answer to the second question is yes. In fact, as pointed out earlier, specifications are often mandatory when developing safety-critical systems.

So how is this seemingly impossible act accomplished? As with most things, writing good specifications is a question of the right people employing a proper method. With the right people I mean people who can serve as the bridge between users and implementers. This means that they should be very well acquainted with the domain, preferably experts, but also have a fair idea of how the specification will be used. When it comes to safety-critical systems such as interlockings, the specification will first serve as input for the implementation; then it will be used as grounds for verification. The implication is that the requirements formulated in the specification should not only be clear and understandable, they should also be verifiable.

As a choice of method, I would go for some kind of formalism, given my habits. However, this is not for everyone. In general, it might be a better way to write the specification in natural language, but with a rigour and precision inspired by formal systems. This includes giving careful descriptions of all the different types of objects mentioned by the requirements. It also includes giving proper definitions of all the particular notions and relations that relate these objects to each other. Having laid such a foundation, the actual requirements can then be written in the clear, understandable and verifiable way we long for.

In the end, never aim for a perfect spec. A decent one will do.

Text and Photo: Daniel Fredholm

Inlägget How to write a decent spec dök först upp på Prover - Engineering a Safer World.