Book
Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science
This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017. The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the practice in verification and testing and are discussing future directions of testing and verification for hardware, software, and complex hybrid systems.
The paper presents MicroTESK, a tool that automates construction of test program generators for microprocessors. A constructed generator consists of the core that implements architecture-independent generation methods and the model that holds information required to generate tests for the corresponding architecture. The tool extracts this information from formal specifications of the instruction set architecture. The extracted information is used in multiple ways: (1) to get the assembly format of the instructions; (2) to build the coverage model of the instruction set architecture; (3) to construct the instruction set simulator used as a reference model. Test programs are created on the basis of test templates provided by users. Flexible architecture of the tool facilitates integration of new test generation engines. MicroTESK has been applied to the ARMv8, MIPS64, PowerPC, RISC-V, and x86 architectures.
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.
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.
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.
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 e ectively 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.
A model for organizing cargo transportation between two node stations connected by a railway line which contains a certain number of intermediate stations is considered. The movement of cargo is in one direction. Such a situation may occur, for example, if one of the node stations is located in a region which produce raw material for manufacturing industry located in another region, and there is another node station. The organization of freight traffic is performed by means of a number of technologies. These technologies determine the rules for taking on cargo at the initial node station, the rules of interaction between neighboring stations, as well as the rule of distribution of cargo to the final node stations. The process of cargo transportation is followed by the set rule of control. For such a model, one must determine possible modes of cargo transportation and describe their properties. This model is described by a finite-dimensional system of differential equations with nonlocal linear restrictions. The class of the solution satisfying nonlocal linear restrictions is extremely narrow. It results in the need for the “correct” extension of solutions of a system of differential equations to a class of quasi-solutions having the distinctive feature of gaps in a countable number of points. It was possible numerically using the Runge–Kutta method of the fourth order to build these quasi-solutions and determine their rate of growth. Let us note that in the technical plan the main complexity consisted in obtaining quasi-solutions satisfying the nonlocal linear restrictions. Furthermore, we investigated the dependence of quasi-solutions and, in particular, sizes of gaps (jumps) of solutions on a number of parameters of the model characterizing a rule of control, technologies for transportation of cargo and intensity of giving of cargo on a node station.
Event logs collected by modern information and technical systems usually contain enough data for automated process models discovery. A variety of algorithms was developed for process models discovery, conformance checking, log to model alignment, comparison of process models, etc., nevertheless a quick analysis of ad-hoc selected parts of a journal still have not get a full-fledged implementation. This paper describes an ROLAP-based method of multidimensional event logs storage for process mining. The result of the analysis of the journal is visualized as directed graph representing the union of all possible event sequences, ranked by their occurrence probability. Our implementation allows the analyst to discover process models for sublogs defined by ad-hoc selection of criteria and value of occurrence probability
Existing approaches suggest that IT strategy should be a reflection of business strategy. However, actually organisations do not often follow business strategy even if it is formally declared. In these conditions, IT strategy can be viewed not as a plan, but as an organisational shared view on the role of information systems. This approach generally reflects only a top-down perspective of IT strategy. So, it can be supplemented by a strategic behaviour pattern (i.e., more or less standard response to a changes that is formed as result of previous experience) to implement bottom-up approach. Two components that can help to establish effective reaction regarding new initiatives in IT are proposed here: model of IT-related decision making, and efficiency measurement metric to estimate maturity of business processes and appropriate IT. Usage of proposed tools is demonstrated in practical cases.