The SCODE method

Thanks to the SCODE method, which is supported and implemented by SCODE-ANALYZER, a formal verification in the tool flags errors in the design of the system, which can then be corrected immediately. Consequently, developers can always work on a formally verified system. Experts can use the results to optimize existing software, design new software, and improve testability.

All results can be further processed in various forms by other tools, including the automatic generation of program code.

The SCODE method

Define problem space

The SCODE method is a three-step iterative process that can easily display and analyze a system. It aims to break a problem down into smaller problems that can be solved independently of each other and to use the solutions to these small problems to resolve the major problem. SCODE-ANALYZER guides the user through the process and actively provides support.

Step 1 – Define the problem space

The first step is to define the problem space, taking into consideration all aspects of the system or the system environment that cause a change in the system (for example, user intervention, measurement results from sensors). Any changes caused (such as modified variables or signals) are seen as output.

Step 2 – Define modes

Define modes

In the second step, valid and invalid system modes are described. Function developers define a mode by combining selected alternatives for each dimension.

Combinations with different input dimensions can produce combinations that have identical output dimensions – in other words, different entries cause the same changes in the system.

SCODE-ANALYZER provides support and checks that all combinations are taken into consideration so that no exceptions are overlooked. This protects against subsequent and costly surprises that arise when, for example, not all requirements were defined at the start. In addition, the software checks that each problem space combination is assigned to a single mode and that there are no overlaps in the definition of the modes.

Step 3 – Define mode transitions

Define mode transitions

In the third step, function developers define how the system is supposed to react when it comes to the transitions between modes. Using a table or graphical user interface, they determine which event triggers a transition from one mode to another. It is also possible to establish that transitions between certain modes are invalid. Developers examine the defined events in the same way as the modes for completeness, deadlocks, and other properties.