Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL*
Despite all the advantages brought by service-oriented architecture (SOA), experts argue that SOA introduces more complexity into information systems rather than resolving it. The problem of service integration challenges modern companies taking the risk of implementing SOA. One of important aspects of this problem relates to dynamic service composition, which has to take into account many types of information and restrictions existing in each enterprise. Moreover, all the changes in business logic should also be promptly reflected. This chapter proposes the approach to solution of the stated problem based on such concepts as model-driven architecture (MDA), ontology modelling and logical analysis. The approach consists of several steps of modelling and finite scope logical analysis for automated translation of business processes into the sequence of service invocations. Formal language of relational logic is proposed as a key element of the proposed approach which is responsible for logical analysis and service workflow generation. We present a logical theory to automatically specialize generic orchestration templates which are close to semantic specification of abstract services in OWL-S. The developed logical theory is described formally in terms of Relational Logic. Our approach is implemented and tested using MIT Alloy Analyzer software.
This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.
This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017. The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as software test automation, static program analysis, verification, dynamic methods of program analysis, testing and analysis of parallel and distributed systems, testing and analysis of high-load and high-availability systems, analysis and verification of hardware and software systems, methods of building quality software, tools for software analysis, testing and verification.
Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In this paper we introduce a uniform tech- nique for checking eectively functionality, k-valuedness, equivalence and inclusion for this model of computation in the case when a semigroup these transducers op- erate over is embeddable in a decidable group.
Finite state transducers extend the finite state automata to model functions on strings or lists. They may be used also as simple models of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. When certain control points are achieved a program outputs the current results of computation as a response. It is significant that different sequences of actions may yield the same result. Therefore, the basic actions of a program may be viewed as generating elements of some appropriate semigroup, and the result of computation may be regarded as the composition of actions performed by the program. This paper offers an alternative technique for the analysis of finite state transducers over semigroups. To check the equivalence of two initial transducers we associate with them a Labeled Transition Systems (LTS). Each path in this LTS represents all possible runs of the initial transducers on the same input word. Every node of the LTS keeps track of the states of the initial transducers achieved at reading some input word and the deficiency of the output words computed so far. If both transducers reach their final states and the deficiency of their outputs is nonzero then this indicates that the initial transducers produce different images for the same word, and, hence, they are not equivalent. The nodes of the LTS that capture this effect are called rejecting nodes. Thus, the equivalence checking of the initial transducers is reduced to checking the reachability of rejecting nodes in the LTS. We show that one needs to analyze only a bounded fragment of the LTS to certify (un)reachability of rejecting nodes. The size of this fragment is polynomial of the size of the initial transducers if both transducers are deterministic, and single-exponential if they are k-bounded. The same approach is applicable for checking k-valuedness of transducers over semigroups.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 invited talks in full paper length. The papers cover various topics in the field of Petri nets and related models of concurrency.
This volume constitutes the refereed proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science, MFCS 2012, held in Bratislava, Slovakia, in August 2012. The 63 revised full papers presented together with 8 invited talks were carefully reviewed and selected from 162 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence.