Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK004.05
Issue:1 (89)
Download PDF0 Kbyte
VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS
Annotation
The paper deals with an interactive method of automatic verification for parallel automata-based programs. The hierarchical state machines can be implemented in different threads and can interact with each other. Verification is done by means of Spin tool and includes automatic Promela model construction, conversion of LTL-formula to Spin format and counterexamples in terms of automata. Interactive verification gives the possibility to decrease verification time and increase the maximum size of verifiable programs. Considered method supports verification of the parallel system for hierarchical automata that interact with each other through messages and shared variables. The feature of automaton model is that each state machine is considered as a new data type and can have an arbitrary bounded number of instances. Each state machine in the system can run a different state machine in a new thread or have nested state machine. This method was implemented in the developed Stater tool. Stater shows correct operation for all test cases.
Keywords
Постоянный URL
Articles in current issue
- PLASMON SOLITONS, KINKS AND FARADAY WAVES IN TWO-DIMENSIONAL LATTICE OF METAL NANOPARTICLES
- STUDY OF CHARACTERISTICS OF SPECTRAL INTERFERENCE SIGNALS IN THE NEAR INFRARED SPECTRAL RANGE
- LOGIC WITH EXCEPTION ON THE ALGEBRA OF FOURIER-DUAL OPERATIONS: NEURAL NET MECHANISM OF COGNITIVE DISSONANCE REDUCING
- EXTRACTION OF MATERIAL PARAMETERS FOR PLASMON MULTILAYER FROM REFLECTION AND TRANSMISSION COEFFICIENTS
- ANALYSIS METHOD OF ANISOTROPIC LIGHTGUIDE h -PARAMETER DEPENDENCE ON ITS BENDING RADIUS
- PROCESS METHODS WITH LOW LEVEL OF OPTICAL LOSSES FOR THE MICROSTRUCTURED FIBER LIGHT GUIDES
- MULTI-ZONE ANTIREFLECTION COATING ON A SUBSTRATE MADE OF OPTICAL ZINC SULPHIDE
- STRUCTURE CONTROL FOR DIFFERENT TYPES OF PAPER BY ATOMIC FORCE MICROSCOPY
- ENERGY-SAVING TECHNOLOGY OF CHEMICAL AGENTS MELTING BY LIGHT RADIATION
- TECHNOLOGICAL IMPERFECTIONS OF FORCE ROD GEOMETRICAL PARAMETERS FOR PANDA OPTICAL FIBERS PRODUCTION
- DATA ANALYSIS BY SQL-MAPREDUCE PLATFORM
- ON THE EFFECT OF ADAPTIVE USER INTERFACES ON RELIABILITY AND EFFICIENCY OF THE AUTOMATED SYSTEMS
- TASKS MAPPING METHOD FOR COARSE GRAIN RECONFIGURABLE SYSTEMS
- IRI-2012 MODEL ADAPTABILITY ESTIMATION FOR AUTOMATED PROCESSING OF VERTICAL SOUNDING IONOGRAMS
- ACCURACY EVALUATION OF THE OBJECT LOCATION VISUALIZATION FOR GEO-INFORMATION AND DISPLAY SYSTEMS OF MANNED AIRCRAFTS NAVIGATION COMPLEXES
- DETECTION OF BACTERIA IN FOODSTUFF BY MACHINE LEARNING METHODS
- DOCUMENT REPRESENTATION FOR CLUSTERING OF SCIENTIFIC ABSTRACTS
- USAGE OF BC7 CONTAINER FOR STORING TEXTURES WITH 10-BIT COLOR DEPTH
- PRELIMINARY AND SUBSEQUENT FILTERING OF NOISE IN IMAGE RESTORATION ALGORITHMS
- RELIABILITY ESTIMATION FOR SCREEN REPRODUCTION OF SATURATED PIGMENTS
- OPERATIONAL CHARACTERISTICS OF INFORMATION SYSTEM SECURITY THREATS RISK
- ANONYMOUS WEBSITE USER IDENTIFICATION BASED ON COMBINED FEATURE SET (WRITING STYLE AND TECHNICAL FEATURES)
- CALCULATION METHODS FOR IRRADIANCE COEFFICIENTS OF CYLINDRICAL SPACE OBJECT BY THE EARTH RADIATION
- OFF-LINE INTERACTION OF THE NONLINEAR DYNAMIC SYSTEMS
- MODERN STATE AND DEVELOPMENT PROSPECTS OF THE BASIC CONCEPTS IN THE FIELD OF MECHATRONICS
- APPLICATION EXPERIENCE AND PROSPECTS OF DIAMOND MICRO-TURNING TECHNOLOGY
- STRAIGHT COGS FORMATION FEATURES FOR CYLINDRICAL SPUR GEARS BY STEPPED GEAR-SHAPED CUTTER
- TEMPERATURE DEPENDENCE CONSIDERATION ISSUE FOR COEFFICIENT OF VOLUMETRIC HEAT CAPACITY IN SIMULATION OF LASER-ARC PAD WELD PROCESS
- METHODS OF TEMPERATURE FIELD MODELING FOR CONTACTLESS LASER DEFORMATION OF A PLATE
- DETACHED-EDDY SIMULATION OF TURBULENT AIRFLOW
- MARKET-MAKING STRATEGY IN THE SYSTEM OF ALGORITHMIC HIGH-FREQUENCY TRADING
- FROM TRADITIONAL DISTANCE LEARNING TO MASS ONLINE OPEN COURSES
- ОБРАТИМАЯ ФОТОДЕСТРУКЦИЯ НАНОЧАСТИЦ СЕРЕБРА В ФОТО-ТЕРМО-РЕФРАКТИВНЫХ СТЕКЛАХ
- EQUATIONS OF RADIATION TRANSFER IN INFRARED TOMOGRAPHY IN THE CASE OF ACTIVE-PASSIVE DIAGNOSIS AND SWEEPING SCANNING
- REAL TIME REGISTRATION OF THE ELECTROPHYSIOLOGICAL SIGNALS SPECTRA