Technology of Symbolic Modeling in Software Engineering

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.
 
 
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 of the needed quality.
Full coverage of model does not allow to be sure of the 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.
 
 
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.
 
 
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 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:
© 2018 LitSoft Enterprise R&D. All Rights Reserved. Designed By JoomLead