Model-Driven Development

ALGEBRAIC APPROACH IN MODEL-DRIVEN DEVELOPMENT

Safety and security software development is critical for the creation of a reliable system especially in avionics, medicine and nuclear industry. The modern process of software development includes different stages where formal methods can be applied. The model-driven development paradigm anticipates the creation of the models as artifacts on every stage of projects like requirements capturing, design stage, coding, testing. It includes such procedures as verification, code generation, and model-based testing.

We propose the life cycle of the development process where we use a number of algebraic models of the system of the different levels of abstraction on every stage for applying the algebraic methods.

WHY ALGEBRAIC (SYMBOLIC) APPROACH?

Among many problems in computer science, there are challenges which face with analyzing of all possible behaviors of models or programs. Such problems are verification, testing, cybersecurity analysis, reverse engineering. Usually, programmers face with the problem of the exponential explosion. During verification and testing activities we try to cover as much behaviors of the program as possible. Big systems have a huge or infinite number of behaviors. Concrete or heuristic methods could not cover all behaviors. The algebraic or symbolic approach allows to process with an infinite number of behaviors and to perform the programs symbolically processing the infinite set of states. For this purpose, we use traditional theories and practice from model checking and our own algebraic achievements developed together with Glushkov Institute of cybernetics: theory of predicate transformer, invariant generation, mixed computations, insertion modeling, enlarged techniques other formal methods. It gave the possibility to provide verification an testing of programs with numerous feature interactions, an enormous number of code lines.

General

The technology of Symbolic Modeling in program engineering uses deductive tools (proving and solving machines or other tools that refer to deductive systems) for processing of sets of system attributes instead of concrete values.

Usage of such technology allows to increase significantly the accuracy of verification or to increase the code coverage during testing that is important for the development of safety-critical or QoS (quality of service) systems.

The development of Safety Critical Systems involves the process of verification for every stage of the standard development process - requirements gathering, system design, coding, testing, integration. The object of the testing could be not only the source code but the formal specifications that present requirements of the design model.

The scheme below shows the more detailed scheme of software development process with verification and testing. The model-driven approach allows proving the code or tests generation procedure at any stage of development. The test suite should correspond to the requested coverage criterion.

The technology of verification and test generation is based on the formal methods that use symbolic modeling. It allows processing with the infinite or large set of states of system or program during testing and verification.

Verification of Formal Specifications

We have to provide the symbolic verification at any stage of software development process if we have the corresponding model of stage artifacts such as - requirements, high level or detailed design model or code. The main properties to be verified, are the following:

- Classical properties of consistency (absence of non-determinism), completeness (absence of deadlocks);

- Safety properties that are defined by a customer for given class of systems;

- Liveness properties;

- Local properties (contracts, annotations) that define correspondence of specifications to requirements or specifications of higher level;

- Classical domain-specific properties - processes races, mutual exclusion, a coherence of states, livelocks.

These properties are checked by usage of the symbolic modeling based on the predicate transformer theory (forward and backward techniques), static checking with proving of satisfiability of formulas of given properties, invariants generation (method of over- and underestimation), static invariants computation.

See our demo:

STAGES OF THE V-MODEL LIFE CYCLE IN SOFTWARE DEVELOPMENT PROCESS

V-model life cycle defines the sequence of processes of development stages and defines the sources of tests for testing procedures that follow after development stages. We consider the model-driven methods, where formal models are the input of every stage and are the objects of verification and test generation.

1. STAGE OF REQUIREMENTS CAPTURING

FLaCon (Formal Languages Converter) provides the conversion from given formal requirements to internal algebraic presentation of SymTech (Behavior Algebra expressions).

Verification of requirements anticipates the following checking:

Static Requirements Checking (incompleteness, inconsistency, liveness and safety properties)

Dynamic Requirements Checking (deadlocks, non-determinisms, annotations).

The level of requirements is the highest level of product specifications. The requirements are used for the process of validation or correspondence of product to customer requirements. Using symbolic technologies it is possible to use generation of symbolic high level tests and automatically run the product under such tests on the final stage. Symbolic tests contain formulas over variables instead parameters.

Generation of code framework. The business logic that presented in requirements could be generated as program code or design specifications.The code will contain contracts (annotations) that inherited from formal requirements.

REQUIREMENTS can be presented from customer as the texts in natural language. Then the process of formalization shall be provided. The formal representation of requirement in SymTech is implemented in UCM (Use Case Maps) and language of Basic Protocols. All they have graphical interpretations.

The formalization language is UCM (Use Case Maps), standardized as part of URN (User Requirements Notation) in ITU-T recommendation (Z.151) which provides a scenario-based approach to requirements specification.

UCM is extended by the language of basic protocols developed at the Glushkov Institute of Cybernetics which represents behavioral requirements as reactions of a system to externally triggered events. Such local behaviors are modeled by basic protocols which consist of three components - pre- and postconditions and process actions.

Pre- and postcondition are represented as formulae of the basic logic language. It supports attributes of numeric and symbolic types, arrays, lists, and functional data types.

The given example shows the formal presentation of textual requirements that describe the work of traffic light.

The order and synchronization of events and basic protocols is defined by means of UCM diagrams in a graphical notation. UCM diagrams are oriented graphs with initial and final states. Nodes of the graph represent events in a system. The basic protocols notation captures the atomic actions (responsibilities) of a UCM map.

2. STAGE OF DESIGN

SymTech anticipates verification and testing of design specifications given as UML diagram and converted by FLaCon to algebraic presentation.

The main procedures implemented on this stage:

Verification of UML diagrams.

Testing of UML diagrams by high level tests.

Generation of code framework (C,Java) (SymTech 2.0).

Checking of annotations inherited from requirements.

Generation of tests for unit or integration testing.

3. STAGE OF CODING

The main procedure implemented on the stage of coding:

Verification of program (standard and given properties).

Checking for vulnerabilities.

Proving of annotations inherited from design stage.

Extraction of business logic.

SymTech 1.0 deals with C, Java, Cobol applications.

4. STAGE OF TESTING

The main procedure implemented on the stage of testing.

- model-based testing with given coverage;

- integration testing;

- symbolic model-based testing of White Box

- cybersecurity testing;

- stress testing.

5. STAGE OF VALIDATION AND SYSTEM TESTING

Testing of product by high-level tests.

Usage of Symbolic Techniques in Testing

It is anticipated that symbolic technique uses proving or solving machine for computation of state or set of states of program system (or model). If we consider the program system or model as transition system with states that are defined by formulas then the new transition will be computed as new formula correspondingly to the transition specification. In the general symbolic technology we compute the possibility to perform transition defining satisfiability of guard formula and compute the new state of the system with the usage of predicate transformers theory.

In the given approach the testing procedure is defined with the usage of the model that is a source of tests. Such approach is known as model-based testing.

Textual requirements are the source for the test model by formalization process. Design model could be considered as test model explicitly.

The test model as an input for test generation tools. The symbolic approach gives the possibility to reach maximal model coverage and to generate symbolic tests that could be converted to concrete tests.

Anyway, there is the number of problems that do not allow to be sure in needed quality.

Full coverage of model does not allow to be sure in full coverage of code lines because of different level of abstraction of code and model.

It is hard to reach the desired results of test coverage for non-deterministic or distributed systems

For the purpose of reaching of maximal code coverage, we consider symbolic white-box testing that is in the scheme below.

In White Box Model-Based Testing we use the source code of system as a source of program behavior scenario (traces) generation. We execute the code symbolically and store the scenario (traces) of its behavior as the sequence of symbolic environment states including input and outputs. Then we use the Model of the system created earlier which contains requested behavior of the system and check obtained traces from System Under Testing for conformance with Model. Test verdict shows the detected issues. Control of program symbolic execution could help to reach requested coverage. The symbolic execution could simulate non-deterministic input.

Demo of MBT algebraic approach:

Integration Testing

Integration testing is important when you have tested the separate module and have integrated it into a whole system that was tested before. For avoiding of full testing of the system it is necessary to define that part of the system which affects the new module and tests this part afterward.

It is implemented by the extraction of the model from the program. The model of the program is presented as behavior algebra expressions.

The symbolic methods are used for the definition of an aspect of the intersection of new module and system correspondingly to common arguments and in test generation. Execution of tests could be performed symbolically with the usage of concrete values in test generation for further usage in test execution systems.

Regression testing

Regression testing is used for avoiding of repetition of test execution of those parts of the code that are not affected by bugs correction after passed test cycle.

The model extraction is also used in this step. Definition of affected attributes of the system or variables of the code is the input for model aspect creation with the following test generation.

ALGEBRAIC APPROACH IN MODEL-DRIVEN DEVELOPMENT

Menu