FIELD: physics.
SUBSTANCE: invention relates to a method for verifying a formal automate model of the behavior of a software system. In the method for constructing a simpler automaton model, a subset of variables of the verified formal automaton model is selected so that part of its events changes only variables that are not included in this subset, variables, invariants and initial states of a simpler automaton model are used; events of a verified formal automaton model are broken into chains of simpler actions, preconditions and postconditions of events are checked in each chain, the execution of invariants of a simpler automaton model in all states thereof is checked, the execution of invariants of a verified formal automaton model in initial states thereof is verified, the execution in all states of the verified formal automaton model invariants, not included in the simple model, is verified, and, based on the results of the checks, a conclusion about the correctness of the model being verified is made.
EFFECT: technical result consists in automating the verification of the correctness of the verified automaton model.
1 cl, 2 dwg
| Title | Year | Author | Number |
|---|---|---|---|
| METHOD OF TESTING MICROPROCESSOR COMPONENTS, TEST ORACLE FOR TESTING MICROPROCESSOR COMPONENTS, TEST ORACLE OPERATION METHOD, METHOD OF CONSTRUCTING TEST ORACLE | 2007 |
|
RU2409839C2 |
| METHOD FOR AUTOMATED PROCESS PREPARATION OF SMALL-SERIES MACHINE BUILDING PRODUCTION TRANSACTION CARDS | 2018 |
|
RU2702387C1 |
| AUTOMATED WORKPLACE OF OPHTHALMOLOGIC MICROSURGEON | 2009 |
|
RU2419133C1 |
| GENERATION METHOD OF KNOWLEDGEBASES FOR SYSTEMS OF VERIFICATION OF DISTRIBUTED COMPUTER COMPLEXES SOFTWARE AND DEVICE FOR ITS IMPLEMENTATION | 2006 |
|
RU2364930C2 |
| SOFTWARE APPLICATION DEVELOPMENT TOOL | 2011 |
|
RU2651883C2 |
| AUTOMATED WORKSTATION FOR OPHTHALMIC MICROSURGEON FOR CONSERVATIVE TREATMENT | 2010 |
|
RU2434264C1 |
| AUTOMATED WORKSTATION FOR ASSESSING QUALITY OF TREATING EYE DISEASES | 2010 |
|
RU2434286C1 |
| AUTOMATED WORKSTATION FOR OPHTHALMIC MICROSURGEON FOR ANTI-GLAUCOMATOSE TREATMENT | 2009 |
|
RU2430404C1 |
| SYSTEM OF MONITORING PRODUCTS/OPERATION WITH HIGH RELIABILITY | 2008 |
|
RU2502081C2 |
| METHOD FOR CONSTRUCTING DIALOGUE MODE IN NATURAL-LIKE LANGUAGE IN SOLVING AUTOMATED CONTROL PROBLEMS IN AUTOMATION TOOL COMPLEXES | 2020 |
|
RU2751435C1 |
