Associated Team proposal (nov 2011)
1. Project Description:
The development of concurrent and parallel systems has traditionally been clearly split in two different families. The first family is based on synchronous models of system behaviour, and is primarily targeted at hardware and circuit design, embedded and reactive systems. Its applications areas have been both involving very expensive design processes (as in processor design for example), but also many safety-critical system problems; as a consequence its development have been very effective in industry, leading to well integrated design methodologies with strong formal basis and elaborated tool support. The second family addresses loosely coupled systems, where communication between distributed entities is asynchronous by nature. Analysis of asynchronous systems has typically greater complexity, because of the greater size of state spaces, has currently attracted lower interest because it was less safety-critical, and has reached lower interest and methodology and tool support in the software industry. However, large and complex asynchronous systems are becoming more and more important, and we see new emerging domains where applications include both synchronous and asynchronous elements. Some approaches have been proposed for relating the two families, starting from GALS (Globally Asynchronous, Locally Synchronous) systems, where reactive synchronous objects where communicating asynchronously; or more recently with PALS (Physically Asynchronous, Logically Synchronous) systems, in which temporal constraints over a layer of asynchronously communication components enable to compute a synchronous abstraction of their behaviour, and to apply synchronous analysis methods at the global level.
We will study modern important topics in information technologies, such as, Internet of Things (IoT), Cloud Computing and Cyber-Physical Systems (CPS). These three topics refer to concurrent and physical parallelism, and may be further refined in: embedded/synchronous and distributed/asynchronous systems (E&DS, shortly). Embedded systems are more focused on runtime stabilization, real-time scheduling and optimization techniques under limited resources, while distributed systems focus rather on large scale organisation and load balancing of distributed communicating computing units. Modern software systems tend to be structured hierarchically in complex designs where multiple embedded systems (manycores, system-on-chips, and sensor networks) are connected by networks and communicate asynchronously. The computing architectures of E&DS are becoming increasingly heterogeneous through time, and they now differ widely according to the target application domain. Examples may be found in Service Oriented Architectures, cloud computing, sensor networks, manycore multiprocessor System-on-Chip architectures, among others. But still, these infrastructures, together with their programming models, share some fundamental concerns: parallelism and concurrency synchronization, determinism and functional correctness, scheduling optimality and calculation time predictability.
2. Expected Outcomes:
Coherent models for synchronous and asynchronous systems:
We shall build on our expertise in terms semantic models respectively for timed andsynchronous systems (Aoste), distributed and asynchronous systems (Oasis), and buildextensions of these models that can be combine in a coherent framework. The idea is not to reinvent from scratch a new framework that would replace existing and well-adopted theories, but rather to keep from each domain their main features and strength, build links between them, and build a coherent framework that will address the Cyber-Physical system
requirements. Concretely, this will give birth to extensions of the respective meta-models (at the level of abstract syntax or meta-models) and of their behavioural semantics. In a second step, extensions or combination of the corresponding modeling tools will be addressed.
Formal model for temporal & spatial consistency:
For real-time systems, many temporal logics have been proposed (timed automata, Timed CCS, Timed CSP, TCTL, Real-Duration Calculus, etc.), good at specifying temporal restrictions for real time systems. A proposal for a clock specification language (CCSL) was made and standardized at OMG as part of the MARTE UML profile; it allows representing such kind of models with engineering model-driven techniques. This project will extend one or more of these logic systems so that they can really describe the integration of computation and physical processes of E&DS. In a second step, prototype tools implementing these formalisms will be developed and connected to our existing analysis tools. More precisely, we want to establish an integrated formal analysis method for specifying the temporal and spatial consistency, combining calculative and physical components, considering collaboration, mobility and heterogeneity. Besides considering constraints of hard real-time and soft-time, we emphasize spatial constraints, namely, how to express the location and how to determine the spatial restrictions thus integrate temporal and spatial constraints to characterize the essential of E&DS.
Task Scheduling:
The E&DS are designed in such a way that collection of various (embedded) computational resources, connected by an interconnection network, collaborated as a single system. In this project, we consider the task scheduling and load balance in the distributed environment with soft real-time limit and pre-emptive priority based on the ASP (Asynchronous Sequential Processes) calculus. These two requirements in distributed systems are now emerging for cyber physical systems (CPS). We want to develop formalized primitives and related scheduling algorithms for task allocation and load balancing with integration of machine performance evaluation, task attributes and scheduling strategy. An important aspect of the aforementioned CCSL formalism is that it allows explicit representation of static regular schedule, as syntactic objects which provide the explicit activation patterns for events and operations. Such features have been proved to match many important cases in classical scheduling theory, such as modulo and affine scheduling as found in process network, nested loop programs with affine bounds, and software pipelining optimization. The periodic subdomain of real-time scheduling can be covered as well (with possibly multirate periods). Dynamic settings with pre-emptive tasks and dynamic priority issues remain problematic, as the ordering now must be established at runtime and cannot be computed and easily encoded into a syntactic pattern beforehand. Opportunities for generalization in dedicated specific cases will be investigated in the course of the project, and form a whole area of research therein.
