Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK004.4’242
Issue:8 (53)
VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER
Annotation
A way to use SPIN verifier for the verification of automata-based programs is proposed. When using this verifier model is described with Promela language and requirements are specified with LTL language. A method of automated automata-based program to Promela model transformation is proposed. For LTL-formulas transformation a special program was developed. Usage of this methods is illustrated on the example of cashmachine model verification.
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 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