О сложности верификации автоматов-преобразователей над коммутативными полугруппами
The article considers the issues of technical product life cycle management in the field of spare parts delivery organization and management within the framework of after-sales service. It provides an examination of a Petri net model, describing the cause-effect relations between events that are linked to delivery planning and management, based on a probabilistic analytical model for after-sales service of technical products and a program-based risk analysis system based on technical and economic criteria. The result of a given model’s performance is planning of an acceptable balance between the cost and quality of products and their current maintenance, which includes detection and minimization of financial risks. An example that illustrates automated planning of spare parts delivery is given. Dynamics of operated technical products’ quantity variation is represented in the integrated graphic type, providing an opportunity to predict an average factor of technical product’s serviceability, determined both by a number of serviceable technical products in a warehouse of the customer and productivity of repair agencies. The earned value method application is proved to be an effective tool for risk analysis of schedule variance in the field of spare parts delivery. Monitoring of the earned value of finances permits to forecast not only the probability of successful completion of spare parts delivery, but also the risks of both cost and schedule variance. An example of automated risk analysis is provided. Estimated coincidence degree of actual cost and planned value is calculated by means of the effectiveness index, which is used to analyze the quality of customer’s subdivisions performance and to correct further functioning. For a selected year, the effectiveness index can be defined and optimized for the predetermined serviceability factor, assigned for every customer during the process of automated planning of spare parts delivery. The approach presented in the article can be considered quite universal, which predetermines an opportunity to apply it in order to provide solutions for product and service life cycle management problems in various organizational technical and economic systems.
This monograph is the collection of the selected papers from Gdańsk EuroSymposium 2015 on SAND – Systems Analysis and Design. SAND is the classical field of research and education in the area of management information systems (MIS) or, as it is called more frequently in Europe – Business Informatics, almost from its origins. The objective of the EuroSymposium on Systems Analysis and Design is to promote and develop high quality research on all issues related to SAND. It provides a forum forSANDresearchers and practitioners in Europe and beyond to interact, collaborate, and develop their field. Therefore, there were three organizers of the 8th EuroSymposium on Systems Analysis and Design: – SIGSAND – Special Interest Group on Systems Analysis and Design of AIS, – PLAIS – Polish Chapter of AIS, – Department of Business Informatics of University of Gdansk, Poland.
Software-dened networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was dened in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specication of SDN forwarding policies, and set up formally model-checking problems for SDNs.
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 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.