Preview

Modeling and Analysis of Information Systems

Advanced search
Vol 18, No 4 (2011)

Articles

7-20 568
Abstract
Atoment is a domain-specific language of executable specifications, used to describe methods and techniques of program verification. In this paper a collection of typical examples of the use of the Atoment language, covering topics such as program models, operational, transformational and axiomatic semantics, formal specification of programming languages is presented.
21-33 570
Abstract
In this paper a new kind of annotations, called attribute annotations, and the methodology for their application in a deductive program verification are proposed. A collection of annotating attributes for the subset C-kernel of the C language is described, and on their base two versions of axiomatic semantics of C-kernel - forward semantics and mixed forward semantics - are presented.
33-44 486
Abstract
One-counter nets are finite-state machines operating on a variable (counter) which ranges over the natural numbers. Every transition can increase or decrease the value of the counter (the decrease is possible only if the result is non-negative, hence zero-testing is not allowed). The class of one-counter nets is equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet contains one symbol. We present a specific method of approximation of the largest bisimulation of a one-counter net, based on the single-periodic arithmetics and a notion of stratified bisimulation.
45-55 586
Abstract
The intention of this paper is to describe a static analysis tool under development. The principal idea behind the design of this tool is to use type and effect systems for static analysis of real programs. The tool uses LLVM bitcode files as input, thus extending the set of analyzed languages to those supported by LLVM compiler infrastructure. It uses its own parser of bitcode files and a program model similar to that of LLVM. The approach taken is to research feasibility of designing instruments for static analysis by applying known type and effect system based algorithms for detecting defects to LLVM bitcode language and effectively to the original source code.
56-67 429
Abstract
Symbolic model checking is based on a compact representation of sets of states and transition relations. At present there are three basic approaches of symbolic model checking: BDD-methods, bounded model checking using SAT-solvers, and various algebraic techniques, for example, constraint based model checking and regular model checking. In this paper we suggest improved algorithms for an algebraic data representation, namely, optimization algorithms for affine data structures.
68-79 536
Abstract
The development of dependency analysis methods in order to improve static code analysis precision is considered in this paper. Reasons for precision loss is abstract interpretation methods when detecting defects in program source code are explained. The need for program object dependency extraction and interpretation is justified by numerous real-world examples. A dependency classification is presented. The necessity for aggregate analysis of values and dependencies is considered. The dependency extraction from assignment statements is described. The dependency interpretation based on logic inference using logic and arithmetic rules is proposed. The methods proposed are implemented in defect detection tool Digitek Aegis and significant increase of precision is shown.
80-93 546
Abstract
The inhibitor Petri net with a fixed structure that executes an arbitrary given Markov normal algorithm was constructed. The algorithm and its input string are encoded by nonnegative integer numbers and put into dedicated places of the Petri net which implements the application of algorithm productions over the string of symbols. The rules of the sequential, branching and cyclic processes encoding by Petri nets were used. At the completion of the net work, the output string is restored (decoded) from the integer form of representation. Within the paradigm of computations on Petri nets the net built provides the compatibility of systems.
94-105 500
Abstract
Hardware/software systems simulated by using the SystemC language are usually parallel and, therefore, may contain synchronization errors. One widespread type of synchronization errors is data races. In this paper we propose an approach to data race detection in SystemC programs which is based on the source code static analysis. We have developed some static analysis algorithms that can extract information for data race detection in a SystemC program without quantitative time. These algorithms can detect all the errors that exist in the program. The efficiency of our approach is shown by the evaluation results of the developed tool on a set of test SystemC programs.
106-117 526
Abstract
An algorithm for solving the coverability problem for monotonic counter systems is presented. The solvability of this problem is well-known, but the algorithm is interesting due to its simplicity. The algorithm has emerged as a simplification of a certain procedure of a supercompiler application (a program specializer based on V.F. Turchin's supercompilation) to a program encoding a monotonic counter system along with initial and target sets of states and from the proof that under some conditions the procedure terminates and solves the coverability problem.
118-130 551
Abstract
The considered model is used in manual development of application specifications and is based on the theory of basic protocols and respective symbolic verification tools. Means to limit the behavioral characteristics of the model still matching the source requirements are discussed. If the model is verified successfully, the executable code of the application and the respective test code are generated from the model. The technique of using the developed model is described.
131-143 720
Abstract
The C language is widely used for developing tools in various application areas, and a number of C software tools are used for critical systems, such as medicine, transport, etc. Correspondingly, the security of such programs should be thoroughly tested, i.e., it is important to develop techniques for detecting vulnerabilities in C programs. In this paper we present an approach for dynamic detection of software vulnerabilities using the SPIN model checker. We discuss how this approach can be implemented in order to detect automatically C code vulnerabilities and illustrate a proposed technique for a number of C programs which are widely used in a number of applications.
144-156 547
Abstract
Uniform systems of communicating extended finite automata are considered in the paper. These automata systems are useful for initial specification of telecommunication systems such as ring protocols and telephone networks. The goal of our paper is to represent an ASV tool (Automata Systems Verifier) intended for analysis and verification of the automata specifications. The ASV tool is based on the algorithm of translation of these automata systems into coloured Petri nets (CPN). This algorithm has been represented and justified in [4]. The ASV tool uses CPN Tools [10] for analysis of the net models and Petri Net Verifier [12] for their verification by the model checking method with respect to properties expressed in mu-calculus. Application of the ASV tool to ring protocol verification and investigation of feature interactions in telephone networks is described.
157-167 528
Abstract
The C program verification project is being developed in IIS. Its latest extension is twofold. First, the labeled variant of axiomatic semantics of the C-kernel language was proposed. The labels, introduced in the calculus, correspond to various concepts inherent in verification conditions (VC). These labels can be extracted from terms and rendered into explanations written in the natural language. User-friendly explanations can play a crucial role in VC understanding and error localization. Second, a subset of the C standard library was specified. The specifications written in ACSL correspond to the C-light memory model. The examples in the paper illustrate the use of these two techniques.
168-180 593
Abstract
The Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes. These themes range from data structures to the complexity theory, but one very special theme is algorithmic design patterns, including greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. Naturally, all the listed design patterns are taught, learned and comprehended by examples. But they can be semi-formalized as design templates, semi-specified by correctness conditions, and semi-formally verified by means of Floyd method. Moreover, this approach can lead to new insights and better comprehension of the design patterns, specification and verification methods. In this paper we demonstrate an utility of the approach by study of backtracking and branch-and-bound design patterns. In particular, we prove correctness of the suggested templates when the boundary condition is monotone, but the decision condition is anti-monotone on sets of "visited" vertices.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)