Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK004.4’242
Issue:5 (69)
ON THE FORMAL SPECIFICATION AND VERIFICATION OF AUTOMATA-BASED PROGRAMS BY SPECIFICATION PATTERNS
Annotation
Model checking is a well developed verification technique; still it is not widely adopted. One of the reasons is that defining formal specification as a set of temporal logic formulae is an error-prone and time-consuming task. This paper gives an overview of the research which focuses on expressing verifiable requirements in a controlled natural language in the framework of automata-based programming. Applicability of the specification patterns in scope of automata-based approach is investigated. Also a formal grammar is introduced to derivate the requirements.
Keywords
Постоянный URL
Articles in current issue
- PARAMETERS RESEARCH OF SUPERFICIALLY COLORED POLYMERIC LENSES
- METHOD FOR ELIMINATING THE NOISE SIGNAL INFLUENCE ON THE SENSITIVITY OF RECEIVING HYDROACOUSTIC ANTENNA BASED ON FIBER BRAGG GRATINGS
- OPTICAL SURFACES PRODUCTION OF ELEMENTS ON THE BASE OF ZINC SULFIDE
- DIGITAL PROCESSING OF FRAUNHOFER DIFFRACTION PATTERNS AT THE OBJECTS GEOMETRICAL PARAMETERS CONTROL
- INVESTIGATION OF MICROSTRUCTURE PARAMETERS OF CHROME FILMS AND THEIR INFLUENCE ON RESULTS OF LOCAL THERMOCHEMICAL OXIDATION BY LASER RADIATION
- THIN METAL FILMS STRUCTURE RESEARCH AFTER FEMTOSECOND LASER RECORDING
- INVESTIGATION OF THE ULTRAVIOLET RADIATION INFLUENCE ON THE THIN FILMS SURFACE
- THE RESEARCH OF THE CONTRAST RASTER CREATION PROCESS BY LASER MARKING
- NONTRIVIAL PENDULUM SYSTEMS CONTROL UNDER CONDITIONS OF PARAMETRIC AND FUNCTIONAL UNCERTAINTIES
- CONTROL SYSTEM SYNTHESIS OF THE ELECTRIC DRIVE OF THE ALTAY TELESCOPE AZIMUTHAL AXIS
- TRANSMISSION AND REFLECTION COEFFICIENTS CALCULATION IN COUPLED QUANTUM WAVEGUIDE SYSTEM
- SOFTWARE PACKAGE FOR PERFORMANCE ANALYSIS OF ALGORITHMS FOR NONLINEAR NAVIGATION PROBLEMS
- THE BALANCING OF RADIAL ELECTROMAGNETIC FORCES OF GATED MOTOR WITH ASYMMETRICAL STATOR WINDING
- TWO-BODY MODEL OF QUANTUM WIRE COUPLED WITH QUANTUM RING
- COMPONENT CALCULATION OF THE SPECTROMETRIC POSITION-SENSITIVE NEUTRON DETECTOR
- ON ELECTROMAGNETIC FIELD INDUCTORS IN JOINT FINITE AND BOUNDARY ELEMENT METHODS
- FORMATION ALGORITHM DEVELOPMENT OF ORDER PACKAGES IN VIRTUAL ENTERPRISES
- HYDROSTATIC PRESSURE IMITATION AT TRIGGER TESTS OF INDEPENDENT UNINHABITED UNDERWATER VEHICLES IN WORKSHOP CONDITIONS
- APPLICATION OF GENETIC PROGRAMMING AND MODEL CHECKING FOR FINITE-STATE MACHINE INDUCTION ON THE BASE OF TESTS AND SPECIFICATION
- GENERATION ALGORITHM FOR 3D FACE MODEL BY A PHOTOGRAPH
- CALCULATIONS OPTIMIZATION IN APPLIED SOFTWARE IN C LANGUAGE ON THE EXAMPLE OF EUROPEAN OPTION PRICING
- THE STATISTICAL ANALYSIS OF NАNOPOROUS GLASSES STRUCTURE BY IMAGES RECEIVED WITH THE METHOD OF CONFOCAL LASER SCANNING MICROSCOPY
- SOLUTION ALGORITHMS FOR DIRECT AND BACKWARD HEAT CONDUCTIVITY PROBLEMS BY MEANS OF DIFFERENTIAL-DIFFERENCE MODELS
- PERSPECTIVE FOR THE DEVELOPMENT OF INNOVATIVE RESEARCH AREAS IN THE FIELD OF LASER SYSTEMS AND BIOMEDICAL OPTICAL TECHNOLOGIES
- METHOD OF DIFFUSE OPTICAL SPECTROSCOPY FOR IN VIVO ESTIMATION OF TUMOR OXYGENATION DYNAMICS
- SUBJECT-ORIENTED LANGUAGES FOR DESCRIPTION OF SCIENTIFIC COMPETITIONS PROBLEMS
- INTERACTIVE TRAINING COMPLEX FOR THE STATE EDUCATIONAL INSTITUTIONS
- COMPETITIVENESS MANAGEMENT PERFECTION OF TRADE ENTERPRISE IN THE CONDITIONS OF SERVICE-ORIENTED ECONOMY
- GENERATED PROBLEMS IN THE SYSTEM INTENDED FOR DISTANCE WORK WITH PROBLEMS
- DEFECTS INVESTIGATION OF SI/SIO2 SYSTEM FORCED BY LASER IRRADIATION
- GaAs P-I-N STRUCTURES FOR X-RAY DETECTORS
- ON CONVERSION OF 32-DIGITS APPLICATIONS INTO 64-DIGITS