Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK004.4’242
Issue:8 (53)
Download PDF0 Kbyte
DEVELOPMENT OF A VERIFIER FOR AUTOMATA-BASED PROGRAMS
Annotation
This article describes verifier of automata-based programs created with the tool to support automatic programming UniMod. When it is used, in contrast to the well-known verifiers, there is no need to describe the model in the input language of the verifier. Requirements for the program are written in the language of temporal logic of linear time LTL (Linear Time Logic). Using this logic verification carried out by intersection of automaton-product of the model and Byuhi automaton built to deny LTL formula.
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
- 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