DIstributed Jointly Operating Networks
We continue to base our research on the Action System formalism, since it has proven useful for modelling distributed systems and hardware systems. We define the mathematical properties, both functional and non-functional, of components within this formalism and use its proof techniques to reason about their behaviour and interaction. Our aim is to develop and investigate the language based issues within the action systems framework. Later they can be adapted to other formalisms, like the B Method.
The correct-by-construction principle can be achieved by stepwise development of an abstract specification or model of a component into a more concrete component proving each refinement step correct relying on Refinement Calculus. In order to help the designer to carry out this construction process systematically we plan to propose action system based transformation rules and dedicated design patterns to be applied in the refinement steps. Similar pre-proven design patterns are also developed within the action systems framework for the process of composing components.
The work on architectural issues on component-based systems has its roots in the coordination paradigm where computation is separated from communication. We plan to continue this line and model components and connectors (i.e. components dedicated to the connection of other components) as well as their interaction within action systems. We believe that the separation of computation and communication concerns helps us to manage the complexity of a derivation as well as assists in developing design patterns for fault tolerance, self-healing and reconfiguration.
Since the Action Systems formalism can be considered to be the basis of the Event B language, we can benefit from the tool support for Event B provided by the RODIN-platform also for Action Systems. Hence, we plan to base the tool support we need for administration of a derivation and proving issues on this platform. Furthermore, we will also investigate the possibility to utilise toolsets of other modelling languages, such as SystemC, BlueSpec, and PROMELA, to implement a tool-assisted Action System-based framework for management of non-functional system properties and constraints.
The project is divided into four work packages, which are described below. The UTU research team will contribute to packets WP2, WP3, and WP4.
WP1:Fundamental research on distributed networks
In this work package we study fundamental properties for distributed networks. Since we are interested in component based design, we will investigate how components can be modelled and designed in a convenient way. When components are composed into systems to run concurrently, their communication becomes an interesting issue. Hence, it is essential to investigate how the components interact, in order to be able to reason about the systems. Furthermore, to increase the parallelism in the composed system, we need to study how the atomicity of the components can be changed. With a higher level of granularity of components, properties like fairness (i.e. that every action gets a chance to be executed) and liveness (i.e. that there is progress in the system) will be important issues to investigate.
WP2:Timing, quality-of-service, energy and complexity
- Investigation of alternative formal models for components and interaction between components and definition of precise models for these suitable for action systems.
- New methods and techniques to reason about atomicity and concurrency with proposals for supporting language constructs and proof patterns for action systems.
- New methods and techniques to reason about fairness and liveness issues for concurrently executing components.
This work package focuses on developing methods for formal modeling, analysis, and management of non-functional properties of a system. Timing issues are problematic especially in complex multiprocessor platforms consisting of several time domains. Quality-of-service (QoS) aspects, e.g. latency and throughput, are of utmost importance for any parallel networked system, including both distributed and network-on-chip systems. Energy and power consumption issues are especially relevant for embedded network-on-chip platforms, but the results of the proposed work will be more generally applicable as well. Energy modelling and estimation requires development of methods to efficiently evaluate computational complexity of formal models. Also area complexity will be addressed as it is an important aspect for networks implemented on a single chip. The concept of time is essential for power consumption analysis, and therefore the work on time-aware modelling can be considered a common nominator of this work package. The following main topics will be investigated and covered:
- New methods to evaluate computational and area complexity of formal component models and a formal system model composed of such component models.
- A methodology to embed physical timing and energy/power information into formal behavioral system component models, to express timing uncertainty as well as temporal and energy/power constraints within our formal framework, and to formally prove if a component model satisfies given physical constraints.
- Formal techniques to explicitly model systems with multiple time domains, interaction between different time domains, and mixed asynchronous-synchronous operation, as well as to analyse energy/power profile of such multi-clocked systems.
- New efficient communication network and protocol modelling techniques for QoS analysis and ensurance, and energy/power estimation of network models.
- Correctness-preserving stepwise refinement of physical timing and energy/power information as a part of networked system refinement, to meet the given physical constraints and network QoS requirements.
- Tool support development for the created Action Systems-based time and energy/power modelling and analysis framework by finding ways to integrate it into existing toolsets of other modelling languages such as SystemC, BlueSpec, B Method, and PROMELA.
It is important to tolerate faults in networked environments. By reconfiguring the network the system may function in a dependable way even if a fault has occurred. Hence, we study how to design self-healing systems that will support network configuration. This issue is essential when dealing with timing and energy consumption issues as described in WP2. The research on self-healing systems will require a more fundamental research on fault tolerance and fault avoidance in system design. Here we initially plan adopt the coordination paradigm.
WP4:Hybrid design approach
- Development of methods and techniques to add different types of fault tolerance mechanisms into formally developed components.
- Investigation of means to model self-healing systems within the action systems formalism and adding these features to components.
We envisage that the foundational research performed in the other work packages will enable us to create high level language constructs and design patterns for the fundamental issues, like atomicity, fairness and liveness investigated in WP1, timing and energy consumption issues in WP2, as well as fault tolerance in WP3. In order to make these constructs and patterns more feasible for the hybrid approach, case studies will be pursued to check their applicability. The case studies will be chosen such that they illustrate the use of the patterns well and point out how the patterns can be further developed. These constructs will then form a library of pre-verified components. The components will be integrated to receive a first version of a hybrid design approach. In the integration we will rely on formal development techniques.
- Development of language constructs and design and proof patterns from the fundamental research issues
- Development of the language constructs and patterns further to better fit into the hybrid approach by applying them on case studies
- Integration of the approaches/language constructs to receive a first prototype of the proposed hybrid approach