This deposit provides the full Carlo multiâengine reasoning architecture, including both the conceptual Codex and the complete pseudocode implementation. Carlo defines a layered system of primitive operators, structural engines, operational cycles, metaâlayer analysis tools, constraint systems, extremeâcase stabilisers, adaptive reasoning modules, and workflow utilities. The entire framework is expressed in plain ASCII for maximum portability, transparency, and remixability. The full set of Carlo engines is useful for anyone exploring complex systems, reasoning architectures, or stateâbased transformations. Each engine contributes a distinct capability: some define primitive operations, some build structure, some manage operational flow, some analyse or predict behaviour, some enforce safety and constraints, some handle extreme conditions, and some adapt the system under stress. Together they form a modular, interoperable toolkit that can model processes, simulate trajectories, test contradictions, stabilise transformations, and support both human and machine reasoning. All components are designed to be readable, composable, and remixable, making the framework suitable for research, experimentation, teaching, prototyping, and building new computational models. This release includes the Carlo Superchain, a unified execution path that chains all engines into one continuous system flow. The Superchain is useful for anyone who wants a single, endâtoâend view of how the entire Carlo Framework runs. It is ideal for researchers, developers, and systems thinkers who need to understand the full lifecycle of a Carlo state, trace how each engine interacts, or build new tools on top of the architecture. The Carlo Super Chain Equation \[\mathcal{S} \;=\; E_n \circ E_{n-1} \circ \dots \circ E_2 \circ E_1\] \[x_{\text{final}} \;=\; \mathcal{S}(x_0)\] \[E_i \;=\; M_i \circ C_i \circ O_i\] \[\mathcal{S} \;=\;(M_n \circ C_n \circ O_n)\circ(M_{n-1} \circ C_{n-1} \circ O_{n-1})\circ\dots\circ(M_1 \circ C_1 \circ O_1)\] \[x_{k+1} \;=\; \mathcal{S}(x_k)\qquadx_k \;=\; \mathcal{S}^k(x_0)\] By chaining every operator, engine, constraint, metaâlayer tool, and adaptive module into one continuous execution flow, the Superchain provides a clear reference model for analysis, implementation, debugging, and experimentation. Because every transformation follows from defined operators and engine rules â with no external assumptions or hidden mechanisms â the Superchain functions as the structural proof of the framework. It demonstrates that the entire Carlo system is coherent, derivable, and complete. Engines: Primitive Operators Engine (core actions: collapse, propagate, reflect, reset) Early Loop Forms Engine (safe looping patterns and stabilisation cycles) Base Constraints Engine (fundamental safety and validity rules) Layering Engine (stacked processing layers that donât overwrite each other) Recursion Engine (safe, bounded recursive transformations) Multi Trajectory Engine (branching into multiple possible futures) State Space Compression Engine (reducing complexity without losing meaning) Carlo Visual Language Engine (ASCIIâsafe symbolic representation) Big Daddy Engine V2 (full structural architecture of the system) Full Nelson Engine (maximumâintensity transformation cycle) Hybrid Engines (structural + operational behaviour combined) Execution Pattern Engines (reusable operator sequences) Operational Engine Wrapper (selects and runs operational modes) Predictive Loop Mapper (forecasts loop behaviour and stability) Contradiction Compass (measures contradiction direction and magnitude) Trajectory Simulator (explores possible futures without choosing one) Cognitive Model (analyses how the system thinks) Meta Layer Engine Wrapper (unified access to all metaâlayer tools) Boundary Engine (keeps values and structures within safe limits) Validity Engine (ensures states are wellâformed and coherent) Loop Safety Engine (prevents infinite or unsafe loops) Collapse Safety Engine (ensures collapse never destroys essentials) State Space Guardrail Engine (prevents explosion or trivial collapse) Constraint Engine Wrapper (runs all constraint checks together) Infinity Engine (handles unbounded growth) Zero Engine (handles collapse to emptiness) Overload Engine (handles too much input or contradiction) Total Contradiction Engine (handles maximum conflict conditions) No Contradiction Engine (prevents overâcompression and stagnation) Degenerate Engine (repairs malformed or broken states) Extreme Case Engine Wrapper (runs all extremeâcase handlers) Fuck Cancer Engine VâOmegaâInfinityâAdaptive (maximum adaptive stabilisation) Adaptive Trajectory Simulator (stressâaware future exploration) Adaptive Cognitive Model (stressâresponsive reasoning analysis) AI Reasoning Engine (adaptive rule interpretation and inference) Adaptive Engine Wrapper (unified adaptive behaviour) Minimal Working Example (smallest runnable Carlo flow) Barebones Template (universal engine skeleton) Universal Execution Flow (master lifecycle of a Carlo state) HTML Rendering Engine (browserânative visualisation) Workflow Engine Wrapper (entry point for workflow tools) Appendices (diagrams, notes, glossary, future extensions) Keywords:Super Chain Loop; CarloâWilliams Engine; Carlo Framework; Carlo Visual Language; Carlo Reset Operator; Carlo Trajectory Simulator; Carlo Cognitive Model; Carlo AI Reasoning Engine; Universal Pseudocode; Engine Architecture; Operator Engine; Loop Dynamics; Recursive Systems; MetaâRecursive Structures; Emergent Behaviour; System Flow Analysis; Computational Physics; Theoretical Computation; Abstract Machine Design; Adaptive Engine Models; Dynamic State Machines; State Transition Logic; HighâOrder Looping; Feedback Loop Theory; Superposition Loops; ChainâLinked Operators; MultiâLayer Engine Design; Extreme Case Demonstrations; Minimal Working Example; Barebones Engine Template; Master Trajectory Update; Observational Tool Order; Predictive Loop Mapper; Contradiction Compass; Emergence Synthesiser; Stability Analysis; Nonlinear Systems; Complexity Theory; Information Flow; Symbolic Computation; Mathematical Modelling; Algorithmic Structures; Process Automation; Simulation Frameworks; PhysicsâCoded Computation; Computational Abstractions; Formal Systems; MetaâSystems Engineering; SelfâReferential Systems; Iterative Engine Design; HighâDimensional Operators; ConstraintâDriven Dynamics; Adaptive Feedback; Systemic Coherence; Structural Invariants; Computational Semantics; Engine Index; Core Definitions; System Overview; Trajectory Mapping; Loop Collapse Theory; Super Chain Loop Mechanics; ChainâLoop Coupling; Nested Loop Structures; Operator Hierarchies; MultiâStage Execution; Execution Pathways; Computational Topology; Symbolic Dynamics; Mathematical Operators; CalculusâLinked Engine Design; Differential System Flow; Integral Loop Behaviour; RateâofâChange Operators; Continuity Constraints; DiscreteâContinuous Hybrid Models; MetaâEngine Construction; Framework Synthesis; Research Tools; Open Science; Zenodo Research; Computational Frameworks; PhysicsâInspired Engines; The Original Loop; Volume Series; Technical Documentation; Engine Specification; Advanced System Design; HighâLevel Abstractions; Scientific Computing; Experimental Frameworks; OpenâSource Engine Research; Future Extensions; Engine Evolution; Adaptive Modelling; CognitiveâInspired Computation; Theoretical Engine Development; Research Infrastructure; Scientific Metadata; Academic Discovery; Knowledge Systems; Computational Reasoning; Symbolic Logic; Formal Verification; System Integrity; Process Coherence; MultiâOperator Chains; Super Chain Loop Integration; EngineâLevel Recursion; Recursive Operator Networks; HighâOrder Engine Behaviour; MetaâLoop Execution; CrossâLayer Dynamics; Computational Architecture; Systemic Feedback; LoopâDriven Computation; EngineâScale Modelling; Abstract Dynamics; Mathematical Foundations; ResearchâGrade Engine Design; Open Research Metadata; Scientific Keywords; Advanced Loop Theory; ChainâReaction Computation; OperatorâLinked Systems; EngineâWide Synchronisation; Temporal Dynamics; Causal Flow Mapping; Structural Loop Analysis; Computational Trajectories; EngineâBased Reasoning; SystemâLevel Abstractions; HighâFidelity Engine Models; Super Chain Loop Expansion; EngineâIntegrated Frameworks; Unified Engine Theory; Computational MetaâFramework; Scientific Engine Toolkit; Carlo Engine Ecosystem
Walter Kurz, Michel Malara, Wojtek Stricker, Eva Albrecht
The objective of this study is to define a compliance-first, conceptually generalisable architecture for a multi-agent artificial intelligence platform integrated with distributed ledger technology, designed to be domain-, deployment-, and vendor-agnostic. It addresses a persistent shortcoming in current AI deployments, where compliance is often treated as a secondary concern, applied retroactively through prompt engineering rather than embedded within the foundational design. The proposed model encodes regulatory, governance, and ESG requirements into an objective-under-constraints framework, ensuring that all specialised agents operate within legally admissible and verifiably auditable parameters prior to any domain-specific implementation. A DAG-based verification layer is incorporated to enable scalable, low-latency, and cost-efficient operation while preserving evidentiary integrity. The analysis evaluates the feasibility of this conceptual model to support sustainable, rapid-deployment vertical applications without inducing vendor lock-in, preserving operational neutrality, and ensuring environmental accountability. The findings suggest that integrating compliance, ESG metrics, and agent specialisation at the architectural level provides a transferable foundation for cross-domain AIâDLT infrastructures.
Dec 23, 2025·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Oliver Alexy, Oliver Baumann, Ying-Ying Hsieh, Giorgia SampĂł
Decentralized Autonomous Organizations (DAOs) represent a radical form of socio-technical systems, where rules are enforced by code and governance is conducted by a distributed network of stakeholders. A critical challenge in designing these systems is achieving consensus without centralized authority, yet how consensus ensures effective governance remains underexplored. This study investigates the design of DAO governance systems, utilizing data from 70 DAOs and applying Fuzzy Set Qualitative Comparative Analysis (fsQCA) to explore which consensus configurations lead to positive organizational outcomes. Our analysis challenges the notion of a single consensus model. Instead, we uncover 13 distinct configurations that characterize successful DAOs. Our key finding reveals a fundamental âideation-legitimation trade-offâ: successful DAOs optimize for broad participation in either the proposal (ideation) stage or the voting (legitimation) stage, but rarely both. These insights provide a nuanced framework for understanding and designing effective governance systems for DAOs.
Distributed Ledger Technology (DLT) engineering practices commonly rely on the adaptation and development of components as key building blocks. However, incorrect component specifications can lead to architectural flaws, which may propagate to implementation stages and result in faulty configurations. To address this, we build on declarative modeling techniques from program verification and refactoring to formally specify DLT components and their architectural composition. We introduce a component-based approach, Alloy4CMD , for the formal modeling and analysis of DLT architectural design. This approach maps individual components into well-formed formal specifications, enabling decidable (bounded) reasoning and property checking. We further employ a lattice-based abstract interpretation to approximate component semantics, with verification carried out in Alloy through assertions expressing conformance to requirements. The analysis involves automated model finding with bounded consistency checks using the Alloy Analyzer. Our approach provides validated, reusable modules, composes them into a validated architectural meta-model that supports early-stage DLT architectural design, and is independent of any particular DLT platform.
The objective of this study is to define a compliance-first, conceptually generalisable architecture for a multi-agent artificial intelligence platform integrated with distributed ledger technology, designed to be domain-, deployment-, and vendor-agnostic. It addresses a persistent shortcoming in current AI deployments, where compliance is often treated as a secondary concern, applied retroactively through prompt engineering rather than embedded within the foundational design. The proposed model encodes regulatory, governance, and ESG requirements into an objective-under-constraints framework, ensuring that all specialised agents operate within legally admissible and verifiably auditable parameters prior to any domain-specific implementation. A DAG-based verification layer is incorporated to enable scalable, low-latency, and cost-efficient operation while preserving evidentiary integrity. The analysis evaluates the feasibility of this conceptual model to support sustainable, rapid-deployment vertical applications without inducing vendor lock-in, preserving operational neutrality, and ensuring environmental accountability. The findings suggest that integrating compliance, ESG metrics, and agent specialisation at the architectural level provides a transferable foundation for cross-domain AI-DLT infrastructures.
Cross-organizational, blockchain-based distributed ledger networks in general, and those based on Hyperledger Fabric in particular, have an architecture which can be adapted to specific application requirements. However, network design can be a particularly challenging task, as the connection between architectural and deployment decisions and extra-functional properties can be subtle and the requirements may contradict each other, requiring trade-offs.
We are currently witnessing the proliferation of blockchain environments to support a wide spectrum of corporate applications through the use of smart contracts. It is of no surprise that smart contract programming language technology constantly evolves to include not only specialized languages such as Solidity, but also general purpose languages such as GoLang and JavaScript. Furthermore, blockchain technology imposes unique challenges related to the monetary cost of deploying smart contracts, and handling roll-back issues when a smart contract fails. It is therefore evident that the complexity of systems involving smart contracts will only increase over time thus making the maintenance and evolution of such systems a very challenging task. One solution to these problems is to approach the implementation and deployment of such systems in a disciplined and automated way. In this paper, we propose a model-driven approach where the structure and inter-dependencies of smart contract, as well as stakeholder objectives, are denoted by extended goal models which can then be transformed to yield Solidity code that conforms with those models. More specifically, we present first a Domain Specific Language (DSL) to denote extended goal models and second, a transformation process which allows for the Abstract Syntax Trees of such a DSL program to be transformed into Solidity smart contact source code. The transformation process ensures that the generated smart contract skeleton code yields a system that is conformant with the model, which serves as a specification of said system so that subsequent analysis, understanding, and maintenance will be easier to achieve.
Research on blockchains addresses multiple issues, with one being the automated creation of smart contracts. Developing smart contract methods is more difficult than mainstream software development as the underlying blockchain infrastructure poses additional complexity. We report on a new approach to developing smart contracts with the objective of automating the process to increase developer efficiency and reduce the risk of errors introduced by software developers. To support industry adoption, we use Business Process Model and Notation (BPMN) modeling to describe an application while targeting applications in the trade vertical. We describe a system that transforms a BPMN model into a multi-modal model that combines Discrete Event (DE) modeling for concurrency with Hierarchical State Machines (HSMs) to represent application functionality. Then, further transformations are used to transform the DE-HSM model into methods in smart contracts. The system lets the modeler decide which of the independent patterns should be transformed into methods of a separate smart contract that is deployed on a sidechain for the purpose of (i) reducing processing costs and/or (ii) providing privacy so that other participants in the smart contract do not have visibility into the processing of the pattern. We also briefly describe a proof-of-concept tool we built to demonstrate the feasibility of our approach.
Seyed Hossein Haeri, Peter Thompson, Neil Davies, Peter Van Roy · 6 authors
This paper directly addresses a long-standing issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply, and reliably whether they can deliver their intended performance before expending significant time, effort, and money on detailed design and implementation. We describe ÎQSD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The distinctive feature of outcome diagrams is that they capture the essential observational properties of the system, independent of the details of system structure and behaviour. The ÎQSD paradigm derives bounds on performance expressed as probability distributions encompassing all possible executions of the system. The ÎQSD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way so that approximate results can be obtained quickly and subsequently refined. ÎQSD has been successfully used by a small team in Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings worth billions of US dollars. The paper outlines the ÎQSD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain. ÎQSD has supported the development of an industry-leading proof-of-stake blockchain implementation that reliably and consistently delivers blocks of up to 80 kB every 20 s on average across a globally distributed network of collaborating block-producing nodes operating on the public internet.
Piero Fraternali, Sergio Luis Herrera GonzĂĄlez, Matteo Frigerio, Mattia Righetti
Distributed Ledger Technology (DLT) is one of the most durable results of virtual currencies, which goes beyond the financial sector and impacts business applications in general. Developers can empower their solutions with DLT capabilities to attain such benefits as decentralization, transparency, non-repudiability of actions and security and immutability of data assets, to the price of integrating a distributed ledger framework into their software architecture. Model-Driven Development (MDD) is the discipline that advocates the use of abstract models and of code generation to reduce the application development and integration effort by delegating repetitive coding to an automated model-to-code transformation engine. In this paper, we explore the suitability of MDD to support the development of hybrid applications that integrate centralized database and distributed ledger architectures and describe a prototypical tool capable of generating the implementation artefacts starting from a high-level model of the application and its architecture.
Seyed Hossein Haeri, Peter Thompson, Neil Davies, Peter Van Roy · 6 authors
This paper directly addresses a critical issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply and reliably whether they will deliver their intended performance before expending significant time, effort and money on detailed design and implementation. We describe ΔQSD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The ΔQSD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way, so that approximate results can be obtained quickly and subsequently refined. ΔQSD has been successfully used by Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings of $Bs. The paper outlines the ΔQSD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain, where application of this approach enabled an advanced distributed proof-of-stake system to meet challenging throughput targets.
Seyed Hossein Haeri, Peter Thompson, Neil Davies, Peter Van Roy · 6 authors
This paper directly addresses a critical issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply and reliably whether they will deliver their intended performance before expending significant time, effort and money on detailed design and implementation. We describe ÎQSD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The ÎQSD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way, so that approximate results can be obtained quickly and subsequently refined. ÎQSD has been successfully used by Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings of $Bs. The paper outlines the ÎQSD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain, where application of this approach enabled an advanced distributed proof-of-stake system to meet challenging throughput targets.
Service fulfillment for clients increasingly involves cooperation between information technology (IT) systems. Designing such solutions requires an architectural approach that ensures symmetry between the communicating parties. For the design of such systems, the author introduces the 1+5 architectural views model. The model contains three new architectural views. For business process modeling, it ensures the integrated processes view. Integration aspects cover two additional views: integrated services, and contracts. Moreover, new stereotypes and tagged values have been added to the unified modeling language (UML). The author has introduced two profiles: UML profile for integration flows, and UML profile for distributed ledger deployment. Communication between systems requires flows that arrange mediation mechanisms. The paper describes an integration flow diagram that extends a UML activity diagram. In the case of blockchain, the author has proposed the smart contract design pattern. The paper describes three case studies that have employed the model to design various solutions. The 1+5 model has proven to be well suited for designing both centralized integration environments with enterprise service bus (ESB) and distributed blockchain solutions with peer-to-peer (P2P) connections.
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.
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.