Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK
Issue:8 (53)
Download PDF0 Kbyte
VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SMV TOOL
Annotation
We consider the method of verification of automata-based programs using Model Checking method. To verify the model the tool SMV is used. In the proposed approach, transition system is not built in explicit form. This allows the program to verify systems with large number of states.
Keywords
Постоянный URL
Articles in current issue
- AUTOMATA-BASED PROGRAMMING PARADIGM
- APPLICATION OF GENETIC PROGRAMMING FOR GENERATION OF AUTOMATA HAVING A LOT OF INPUT VARIABLE
- APPLICATION OF GENETIC PROGRAMMING, FINITE STATE MACHINES AND NEURAL NETS FOR CONSTRUCTION OF CONTROL SYSTEM FOR UNNMANED AIRCRAFT
- APPLICATION OF GENETIC PROGRAMMING AND OF REDUCED TRANSITION TABLES METHOD AND OF DECISION TREES METHOD FOR CONSTRUCTING A CONTROL SYSTEM FOR A MODEL OF AN UNMANNED AIRCRAFT
- CONSTRUCTION OF A CONTROL SYSTEM FOR A HELICOPTER MODEL USING GENETIC ALGORITHMS
- CONSTRUCTION OF A CONTROL SYSTEM FOR ROBOCODE TANK USING GENETIC ALGORITHMS
- DEVELOPMENT OF A TOOL FOR FINITE STATE MACHINE GENERATION WITH GENETIC ALGORTIHMS
- A METHOD OF REPRESENTING AUTOMATA WITH DECISION TREES FOR GENETIC PROGRAMMING
- APPLICATION OF GENETIC ALGORTIHMS FOR MOORE AUTOMATA AND SYSTEMS OF MEALY AUTOMATA CONSTRUCTION IN “ARTIFICIAL ANT” PROBLEM
- METHODS FOR OPTIMIZATION OF GENETIC ALGORITHMS CONSTRUCTING FINITE STATE MACHINES
- METHODS OF AUTOMATA-BASED PROGRAMS VERIFICATION
- VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SMV TOOL
- VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER
- VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL
- DEVELOPMENT OF A VERIFIER FOR AUTOMATA-BASED PROGRAMS
- APPLICATION OF AUTOMATA-BASED APPROACH FOR JAVA CARD-APPLICATIONS DEVELOPMENT
- DEVELOPMENT OF CORECT JAVA CARD-APPLICATION WITH AUTOMATA-BASED APPROACH
- VERIFICATION OF INTERACTION OF PARTS OF A REACTIVE SYSTEM IMPLEMENTED USING AUTOMATA-BASED APPROACH
- AUTOMATIC DYNAMIC VERIFICATION OF AUTOMATA-BASED PROGRAMS
- DECLARATIVE APPROACH TO EMBEDDING AND INHERITANCE OF AUTOMATA CLASSES WITH IMPERATIVE PROGRAMMING LANGUAGES
- INHERITANCE OF AUTOMATA CLASSED WITH DYNAMIC PROGRAMMING LANGUAGES ON THE EXAMPLE OF RUBY
- A TOOL SUPPORTING AUTOMATA-BASED PROGRAMMING – UNIMOD 2. DESIGN. VALIDATION. VERIFICATION. IMPLEMENTATION
- TEXTUAL LANGUAGE FOR AUTOMATA-BASED PROGRAMMING
- TEXTUAL LANGUAGE FOR AUTOMATA-BASED PROGRAMMING FSML FOR UNIMOD TOOL
- A METHOD OF TESTS FOR API GENERATION ON THE BASE OF FINITE-STATE MODEL OF TESTING
- APPLICATION OF AUTOMATA-BASED APPROACH FOR A MOBILE ROBOT CONTROL SYSTEM
- APPLICATION OF FINITE STATE MACHINES FOR AUTOMATIZATION OF DOCUMENTS CIRCULATION
- A MACHINE LEARINIGN METHOD FOR COMPLX SYSTEMS WITH A LOT OF INPUT DATA AND OUTPUT ACTIONS