In critical systems, failures or errors can cause catastrophes, such as deaths or considerably losses of money. Model checking provides an automated way to prove the correctness of programs' requirements. It is a convenient technique to use in systems that need reliability. Propositional Dynamic Logic (PDL) is a formal system designed to reason about programs. This work presents a compiler implementation from a subset of the C language and also for the Smacco model, both to the PDL language, and after that to the language of the nuXmv model checker. This implementation is linked with a Blockchain model generation system to model and reason about smart contracts.
Decentralized systems have been widely developed and applied to address security and privacy issues in centralized systems, especially since the advancement of distributed ledger technology. However, it is challenging to ensure their correct functioning with respect to their designs and minimize the technical risk before the delivery. Although formal methods have made significant progress over the past decades, a feasible solution based on formal methods from a development process perspective has not been well developed. In this paper, we formulate an iterative and incremental development process, named formalism-driven development (FDD), for developing provably correct decentralized systems under the guidance of formal methods. We also present a framework named Seniz, to practicalize FDD with a new modeling language and scaffolds. Furthermore, we conduct case studies to demonstrate the effectiveness of FDD in practice with the support of Seniz.
Christian Berger, Birgit Penzenstadler, Olaf Drögehorn
Innovation in the world of today is mainly driven by software. Companies need to continuously rejuvenate their product portfolios with new features to stay ahead of their competitors. For example, recent trends explore the application of blockchains to domains other than finance. This paper analyzes the state-of-the-art for safety-critical systems as found in modern vehicles like self-driving cars, smart energy systems, and home automation focusing on specific challenges where key ideas behind blockchains might be applicable. Next, potential benefits unlocked by applying such ideas are presented and discussed for the respective usage scenario. Finally, a research agenda is outlined to summarize remaining challenges for successfully applying blockchains to safety-critical cyber-physical systems.
M. Teresa Higuera‐Toledano, Uwe Brinkschulte, Achim Rettberg
The increasing complexity of contemporary embedded computing systems requires the use of self-management in order to handle unforeseen changes in both hardware and application environments (i.e., hardware/software defects, resource changes, and non-continual feature usage). Moreover, often these systems are distributed, running on processor architectures with multiple cores, which may require self-organization to ensure efficiency and reliability. Real-time properties are another key issue in many complex systems. Adaptive and self-organized properties extent the area of operations and improves the efficiency of the system resources at the cost to introduce additional complexity, overhead, and resource requirements. Consequently, real-time adaptive systems must be careful analyzed, designed, and built taken into account the right tradeoffs between flexibility and complexity, while accomplishing time-constrains. The combination of the flexibility and uncertain behavior of self-organizing systems with time-predictability is a grand challenge. Therefore, substantial research has been done in the last years to address the so-called Self-X features (e.g., self-configuration, self-optimization, self-adaptation, self-healing, and self-protection). This fact has as resutl that self-organizing computing systems become an established research nowadays as they promise to handle the increasing complexity resulting from highly distributed systems and ubiquitous applications. In addition, real-time properties are required in many areas (such as cyber physical systems) self-organizing computing systems are dealing with. Combining the flexible and and uncertain behavior of self-organizing systems with time-predictability necessary for real-time systems is a grand challenge. The Workshop on Self-Organizing Real-Time Systems (SORT) is specifically dedicated to research on adaptive real-time systems. SORT started 2014 as a workshop attached at International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC). The purpose of this workshop is to provide an open forum to discuss new and ongoing research that is centered on the idea of adaptability in real-time systems. The target audience includes researchers from academia, tool vendors, system suppliers, and users in industry who are interested in the all aspects of the topics mentioned below. This special issue of Concurrency and Computation: Practice and Experience contains four invited papers from the SORT 2014 workshop that has been expanded and carefully peer reviewed. The first paper, titled An Artificial DNA for Self-Descripting and Self-Building Embedded Real-Time Systems 1, Uwe Brinkschulte proposes an approach to use an artificial DNA-based approach for embedded real-time and distributed systems. This kind of systems is growing more and more complex because of the increasing chip integration density, larger number of chips in distributed applications and demanding application fields (e.g., in cars and in households). Bio-inspired techniques like self-organization are a key feature to handle this complexity. Because many embedded systems can be composed from a limited number of basic elements, the structure and parameters of such systems can be stored in a compact way representing an artificial DNA deposited in each computation node. This leads to a self-describing system. Based on the DNA, the self-organization mechanisms can build the system autonomously providing a selfbuilding system. System repair and optimization at runtime are also possible, leading to higher robustness, dependability, and flexibility. Autonomous adaptation in self-adapting embedded real-time systems introduces novel risks as it may lead to unforeseen system behavior. An anomaly detection framework integrated in a real-time operating system can ease the identification of such suspicious novel behavior and, thereby, offers the potential to enhance the reliability of the considered self-x system. However, anomaly detection is based on knowledge about normal behavior. When dealing with self-reconfiguring applications, normal behavior changes. Hence, knowledge base requires adaptation or even reconstruction at runtime. The stringent restrictions of real-time systems considering runtime and memory consumption make this task to a really challenging problem. In next paper, Two-Level Extensions of an Artifical Hormone System 2, Mathias Pacher describes a decentralized software which is able to allocate tasks in a system of heterogeneous processing elements. Tasks are allocated according to their suitability for the heterogeneous processing elements, the current processing element and task relationships. This software provides properties like self-configuration, self-optimization, and self-healing in the context of task allocation. In addition, it is able to guarantee real-time bounds for such self-X-properties. However, using self-organization principles introduces increased system complexity such as control of system parameters for self-organization and additional communication effort, which have been addressed by using a hierarchic structure. This solution uses a machine learning approach presenting an Observer-/Controller architecture. The user has to provide a simple set of initial rules and the Observer-/Controller is able to generate new rules if needed. This paper also presents a hierarchical structure to save communication bandwidth, which consists of several different clusters of processing elements where each cluster has its own communication infrastructure (e.g., a bus system). In the paper titled Online behavior classification for anomaly detection in self-x real-time systems 3, Katharina Stahl presents an online construction of application behavior knowledge that does not rely on training phase. The applications' behavior is defined by the application's system call invocations. For the knowledge base, they use Suffix Trees to represent application behavior patterns and associated information in a compact manner. The online algorithm provided by Suffix Trees is a basis to construct the knowledge base with low computational effort. Anomaly detection and classification is integrated into the online construction method. New behavioral patterns do not unconditionally update the behavior knowledge base. They are evaluated in a context-related manner inspired by Danger Theory, a special discipline of Artificial Immune Systems. For highly safety-critical applications, rigorous offline verification should be complemented by online verification. One promising technique is Online Model Checking (OMC). As OMC is a run- time-provided service, it seems to be natural providing it by an operating system service like any other service offered by the OS. In the paper titled Efficient Integration of Online Model Checking into a Small-Footprint Real-time Operating System 4 the authors study the feasibility of integrating OMC as an RTOS service. In order to ease understanding the approach, the paper discusses various integration methods in which OMC runs concurrently to the application task to be online model checked. The OMC may become: (i) an integral part of the RTOS, (ii) a separate task running on the same host as the RTOS, or (iii) a remote host as a kind of service-oriented architecture.
Large-scale organizations, such as Siemens, develop a broad field of products for varying domains. Software constitutes a major innovation and cost factor to their development. Organizational-wide reuse of software across products, even across domains, gives these organizations a competitive advantage. This involves large-scale reuse approaches where software is developed in a decentralized manner by several internal, yet self-contained organizational units -- those units are separate profit centers with own business objectives, organizationally independent with own product management, and have widely autonomous processes and software-engineering life cycles. I define those systems as internal software ecosystems. The intra-organizational, yet decentralized development context increases the amount and complexity of dependencies among both software assets and the responsible organizational units. This significantly impacts collaboration in software engineering. Traditional process-centric coordination mechanisms become increasingly inefficient, calling for a suitable software architecture to enable effective collaboration. However, in order to make informed architecture decisions, applied modes of collaboration and resulting architecture challenges must be understood. As first major contribution in this thesis, I provide strong empirical evidence on collaboration and resulting architecture challenges for two of the largest internal software ecosystems at Siemens -- based on a total of 46 hours of semi-structured interviews with 17 leading software architects from all involved organizational units. I identify three collaboration models on a continuum that ranges from high to low coupling and a classification of architecture challenges together with a qualitative and quantitative exposure of the identified recurring hurdles. My results outline a broad field of real-world challenges that need to be investigated by researchers, and my results support practitioners who follow the collaboration models to make informed architecture decisions based on empirical evidence. Besides taking informed architecture decisions, it is equally important to manage and control adherence to the specified architecture at an ecosystem-wide level. However, feature and schedule pressure regularly require to accept architecture violations by several organizational units, which decreases quality and increases maintenance costs. As main finding of my investigation on collaboration and architecture challenges, I identify the explicit and systematic management of architecture violations as the key challenge for internal software ecosystems, in particular the lack of developer support for resolving violations. As second major contribution within this thesis, I elaborate the TrAViM approach, a framework that comprises seven violation-management capabilities for internal software ecosystems. Their main purpose is developer support for resolving architecture violations, aiming to reduce the developers' effort required to handle them. I develop a prototype that instantiates the approach. Using the prototype, I conduct an in-depth case study on the capabilities' usefulness, involving 9 experts from my study systems. All of them expressed that the capabilities are highly valuable and hold great potential to ease violation management for large-scale software engineering.
Self-organization provides a suitable model for developing self-managed complex distributed systems, such as grid computing and sensor networks. Unlike current related studies, which propose only a single principle of self-organization, this mechanism synthesizes the three principles of self-organization: cloning/ spawning, resource exchange and relation adaptation. Based on this mechanism, an agent can autonomously generate new agents when it is overloaded, exchange resources with other agents if necessary, and modify relations with other agents to achieve a better agent network structure. In this way, agents can adapt to dynamic environments. The proposed mechanism is evaluated through a comparison with three other approaches, each of which represents state-of-the-art research in each of the three self-organization principles. Experimental results demonstrate that the proposed mechanism outperforms the three approaches in terms of the profit of individual agents and the entire agent network, the load-balancing among agents, and the time consumption to finish a simulation run. In addition, in a dynamic environment, it is nearly impossible to use a static, design time generated system structure for efficient problem solving. Instead, the system needs to be able to self-organize at runtime, which means that the components of the system are responsible for adapting themselves to suit the dynamic environment. Self-organization is usually defined as "the mechanism or the process enabling the system to change its organization without explicit external command during its execution time.
The realization of large and complex cyber-physical systems (such as "smart" transportation, energy, security, and health-care systems) is creating design and verification challenges which will soon become insurmountable with the current engineering practices. These highly heterogeneous systems, tightly combining physical processes with computation, communication, and control elements, would substantially benefit from hierarchical and compositional methodologies to make their design possible let alone optimal. Several languages and tools have been proposed over the years to enable model-based development of complex systems. However, an all-encompassing design framework that helps interconnect different tools, possibly operating on different system representations, is still missing.In this dissertation, we introduce a design methodology that addresses the complexity and heterogeneity of cyber-physical systems by using assume-guarantee contracts to formalize the design process and enable the realization of system architectures and control algorithms in a hierarchical and compositional way. In our methodology, components are specified by contracts, and systems by compositions of contracts. Contracts explicitly define the assumptions of a component on its environment and the guarantees of the component under these assumptions. Contract operations and relations, such as composition, conjunction and refinement allow proving that: (i) an aggregation of components are compatible, i.e. there exists a legal environment in which they can operate; (ii) a set of specifications are consistent, i.e. there exists an implementation satisfying all of them; (iii) an aggregation of components refines a specification, i.e. it implements the specification contract and is able to operate in any environment admitted by it. While horizontal contracts are used to specify components and aggregations of components at the same level of abstraction, we introduce the notion of vertical contracts to reason about richer refinement relations and mappings between different abstraction levels, possibly described by heterogeneous architectures and behavior formalisms. Moreover, we further investigate the problem of compatibility for systems with uncontrolled inputs and controlled outputs, by establishing a link between the theory of contracts and the one of interfaces, which rely on different mathematical formalisms, while sharing the same objectives. From this link, we derive a new projection operator on contracts that enables the preservation of the semantics of interface composition and compatibility.Resting on the above contract framework, the design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. To allow for requirement analysis and early detection of inconsistencies, top-level system requirements are captured as contracts, by leveraging a front-end pattern-based specification language and a set of back-end formal languages, including mixed integer-linear constraints and temporal logic. Top-level contracts are then refined to achieve independent development of system architectures and control algorithms, by combining synthesis from requirements and optimization methods.To enable efficient architecture selection under safety and reliability constraints, we explore two optimization-based methods that use an approximate reliability analysis technique to overcome the exponential complexity of exact computations. The Integer-Linear Programming with Approximate Reliability (ILP-AR) method generates larger, monolithic optimization problems using approximate but efficient reliability computations with an explicit theoretical bound on the error. Conversely, the Integer-Linear Programming Modulo Reliability (ILP-MR) method breaks the complex architecture selection task into a sequence of smaller optimization tasks without reliability constraints, interleaved with exact reliability checks. By relying on efficient mechanisms to prune out candidate architectures that are inconsistent with the reliability constraints, ILP-MR can run faster than ILP-AR on large problem instances.We further explore two methods to systematically design control strategies for a given architecture. The reactive synthesis-based optimal control mapping (RS-OCM) method generates controllers by combining reactive synthesis from linear temporal logic contracts with optimization techniques based on simulation and monitoring of signal temporal logic contracts. Different design concerns are then addressed by leveraging the most appropriate abstraction levels, using contracts from the pre-characterized library to accelerate verification tasks. The programming-based optimal control mapping (P-OCM) method uses, instead, a discrete-time representation of the system and a formalization of the design requirements in terms of arithmetic constraints over real numbers to cast the control problem as an optimization problem over a finite time horizon. The optimization problem is then solved with a receding horizon approach and scales better than monolithic reactive synthesis from linear temporal logic.We demonstrate, for the first time, the effectiveness of a contract-based design flow on real-life examples of industrial relevance, namely, the design of aircraft electric power distribution and environment control systems. In our framework, optimal selection of large, industrial-scale power system architectures can be performed in a few minutes. Design validation of power system controllers based on linear temporal logic contracts shows up to two orders of magnitude improvement in terms of execution time with respect to conventional techniques. Finally, our optimization-based load management scheme allows better resource utilization than a conventional one.
Ramachandra Kota, Nicholas Gibbins, Nicholas R. Jennings
Self-organizing multi-agent systems provide a suitable paradigm for developing autonomic computing systems that manage themselves. Towards this goal, we demonstrate a robust, decentralized approach for structural adaptation in explicitly modeled problem solving agent organizations. Based on self-organization principles, our method enables the autonomous agents to modify their structural relations to achieve a better allocation of tasks in a simulated task-solving environment. Specifically, the agents reason about when and how to adapt using only their history of interactions as guidance. We empirically show that, in a wide range of closed, open, static, and dynamic scenarios, the performance of organizations using our method is close (70–90%) to that of an idealized centralized allocation method and is considerably better (10–60%) than the current state-of-the-art decentralized approaches.
Antonia Bertolino, Guglielmo De Angelis, Antonino Sabetta, Andrea Polini
Service Oriented Architecture (SOA) is changing the way in which software applications are designed, deployed and maintained. A service-oriented application consists of the runtime composition of autonomous services that are typically owned and controlled by different organizations. This decentralization impacts on the dependability of applications that consist of dynamic services agglomerates, and challenges their validation. Different techniques can be used or combined for the verification of dependability aspects, spanning over traditional off-line testing approaches, monitoring, and on-line testing. In this chapter we discuss issues and opportunities of SOA validation, we identify three different stages for validation along the service life-cycle model, and we overview some proposed research approaches and tools. The emphasis is on on-line testing, which to us is the most peculiar stage in the SOA validation process. Finally, we claim that on-line testing is only possible within an agreed governance framework.
A key challenge for software engineering is to learn how to reconcile the formal world of the machine and its software with the non-formal real world. In this paper, we describe Problem Oriented Software Engineering (POSE), an approach that brings both non-formal and formal aspects of software development together within a single theoretical framework for software engineering design. We show how POSE captures development as the recordable and re-playable design theoretic transformation of software problems. Their representation and transformation allows for the identification and clarification of system requirements, the understanding and structuring of the problem world, the structuring and specification of a hard-ware/software machine that can ensure satisfaction of the requirements in the problem world, and the construction of adequacy arguments, convincing both to developers and to customers, users and other interested stake-holders, that the system will provide what is needed. Designs are recordable and re-playable through our adaptation of tactics, a (now standard) form of programming language used in transformational proof theoretic presentations. This brings to our system many other benefits of such approaches, including the ability to abstract from a captured design, and to combine programmatically captured designs. This paper provides an example-driven presentation of our framework for software engineering design.
Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. We extend smart play-out to cover a larger set of the LSC language features and to deal more efficiently with larger models. The extensions cover two key features of the rich version of LSCs, namely, time and forbidden elements. The former is crucial for systems with time constraints and/or time-driven behavior, and the latter allows specifying invariants and contracts on behavior. Forbidden elements can also help reduce the state space considered, thus enabling smart play-out to handle larger models.
We develop a formal multi-agent system based on a modal algebra enabling us to preserve the essential characteristics of its autonomous software agents (autonomy, mobility, etc.), as well as to explore the formal properties and management of the cooperations (non-hierarchical or flat structures) and coordinations (hierarchical structures) among those simple agents, that can be constructed through the operations of the model. We show the potential of these operations that allow us to construct different cooperations and coordinations based on the same set of autonomous agents (as alternative solutions with respect to the same given problem), while, in parallel we provide the means in order to explicitly specify different types of coordinated flows of information specified and governed by these structures. We illustrate all the above via a number of algorithms referring to the development of a simple (in structure) data mining system. We simply selected an adequate application area with no purpose to compare data mining methods and techniques. The various algorithmic solutions we suggest, unveil the resilience of the alternative design approaches aiming at improving issues like decentralization of services, as well as enhancing performance through concurrent organization by thus exploiting the different possibilities of the model.
Argumentation is receiving an increasing attention as a technique for practical and uncertain reasoning underlying the realization of intelligent autonomous agents. Since a decentralized organization has been proposed by several authors as an appropriate paradigm for the design of agent architectures, we propose in this article, a distributed approach to argumentation, in which several independent asynchronous processes carry out argumentation activity, by exploiting local information only. The final result of this process is the computation of the defeat status of the arguments: we devise a general distributed algorithm, which does not rely on any specific notion of defeat between arguments. The issue of coordination has been explicitly tackled by ensuring the property of self-stabilization for the algorithm. A proof of its correctness, as well as an analysis of its complexity, is provided.