The main features of Platform SymTech 1.0 are

- testing technologies;

- model-driven development;

- support of development process of critical system or system with Quality of Service (QoS);

- verification and validation;

- cybersecurity.

SymTech 1.0 is the system with the usage of Symbolic Technology that involves algebraic and deductive formal methods for resolving of sophisticated industrial challenges.

The platform SymTech 1.0 is intended for supporting of software development process for the industrial critical system in telephony and telecommunication, automotive industry, telecommunications, military, avionics. It is the software lineup that includes verification and testing systems, symbolic modeling tools, libraries for the creation of necessary business configuration for successful implementation of software development process. It is compatible with such life cycles as V-model, waterfall model of CMMI standard. It supports software process at every stage of development starting from requirements capturing to testing activities. Version SymTech 1.0 is experimental and used by specially trained people for support of software development process in IT companies. It is anticipated that SymTech 2.0 will be available via web-interface and the version SymTech 3.0 could be used within the cloud.



Among the 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 heuristics methods could not cover all behaviors. The algebraic or symbolic approach allows to process with an infinite number of behaviors and 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.




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.



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 is implemented in UCM (Use Case Maps) and language of Basic Protocols. All they have the 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.



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.



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.



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.


Detail description of testing methods with usage of symbolic techniques is in TESTING TECHNOLOGIES.



Testing of product by high-level tests.

© 2018 LitSoft Enterprise R&D. All Rights Reserved. Designed By JoomLead