Search

International audience; Major challenges in the software development of distributed systems are rooted in the complex nature of coordination. Assertions are a practical programming mechanism to improve the quality of software in general by monitoring it at runtime. Most approaches today limit assertions to statements about local states whereas coordination requires reasoning about distributed states. The Peer Model is an event-based coordination programming model that relies on known foundations like shared tuple spaces, Actor Model, and Petri Nets. We extend it with distributed runtime invariant assertions that are specified and implemented using its own coordination mechanisms. This lifts the concept of runtime assertions to the level of coordination modeling. The concept is demonstrated by means of an example from the railway domain.

International audience; The Peer Model is a model for the specification of coordination aspects found in concurrent and distributed systems. It provides modeling constructs for flows, time, remoting and exception handling. The main concepts of the ground model are peers, wirings, containers, entries and services. Its intent is to introduce specific modeling abstractions of concurrency and distribution to make designs more readable and suitable for larger problems. However, there still exist coordination aspects that are not straight forward to model with it. In this paper, therefore the Peer Model is extended by modeling constructs for nested, distributed transactions based on the Flex transaction model. This approach eases the advanced control of structured and distributed coordination scenarios that have to cope with complex, dependent and concurrent flows. The evaluation introduces a coordination challenge that requires adaptive and transactional distribution of resources, dependencies between concurrent activities, error handling and compensation. It demonstrates the improvements that can be achieved with the new modeling concepts.

International audience; Book Front Matter of LNCS 8459

International audience; Modern distributed software systems must integrate in near-time parallel processes and heterogeneous information sources provided by active, autonomous software systems. Such lively information sources are e.g. sensory data, weather data, traffic data, or booking data, operated by independent distributed sites. The complex integration requires the coordination of these data flows to guarantee consistent global semantics. Design, implementation, analysis and control of distributed concurrent systems are notoriously complex tasks. Petri Nets are widely used to model concurrent activities. However, a higher-level programming abstraction is needed. We propose a new programming model for modeling concurrent coordination patterns, which is based on the idea of “peer workers” that represent re-usable coordination and application components. These components encapsulate behavior, structure distributed data and control flow, and allow integration of pre-existing service functions. A domain-specific language is presented. The usability of the peer-based programming model is evaluated with the Split/Join pattern.

A session-based process satisfies the progress property if its\ud sessions never get stuck when it is executed in an adequate context.\ud Previous work studied how to define progress by introducing the notion of\ud catalysers, execution contexts generated from the type of a process. In\ud this paper, we refine such definition to capture a more intuitive notion\ud of context adequacy for checking progress. Interestingly, our new catalysers\ud lead to a novel characterisation of progress in terms of the standard\ud notion of lock-freedom. Guided by this discovery, we also develop a\ud conservative extension of catalysers that does not depend on types, generalising\ud the notion of progress to untyped session-based processes. We\ud combine our results with existing techniques for lock-freedom, obtaining\ud a new methodology for proving progress. Our methodology captures new\ud processes wrt previous progress analysis based on session types.

International audience; Message passing provides a powerful communication abstraction in both distributed and shared memory environments. It is particularly successful at preventing problems arising from shared state, such as data races, as it avoids sharing in general. Message passing is less effective when concurrent access to large amounts of data is needed, as the overhead of messaging may be prohibitive. In shared memory environments, this issue could be alleviated by supporting direct access to shared data; but then ensuring proper synchronization becomes again the dominant problem. This paper proposes a safe and efficient approach to data sharing in message-passing concurrency models based on the idea of distinguishing active and passive computational units. Passive units do not have execution capabilities but offer to active units exclusive and direct access to the data they encapsulate. The access is transparent due to a single primitive for both data access and message passing. By distinguishing active and passive units, no additional infrastructure for shared data is necessary. The concept is applied to SCOOP, an object-oriented concurrency model, where it reduces execution time by several orders of magnitude on data-intensive parallel programs.

International audience; Event-Condition-Action (ECA) rules are a widely used language for the high level specification of controllers in adaptive systems, such as Cyber-Physical Systems and smart environments, where devices equipped with sensors and actuators are controlled according to a set of rules. The evaluation and execution of every ECA rule is considered to be independent from the others, but interactions of rule actions can cause the system behaviors to be unpredictable or unsafe. Typical problems are in redundancy of rules, inconsistencies, circularity, or application-dependent safety issues. Hence, there is a need for coordination of ECA rule-based systems in order to ensure safety objectives. We propose a tool-supported method for verifying and controlling the correct interactions of rules, relying on formal models related to reactive systems, and Discrete Controller Synthesis (DCS) to generate correct rule controllers.