Abstract
Concurrent programming is dominated by thread based solutions with lock based critical sections. Careful attention has to be paid to avoid race and deadlock conditions. Real-Time for The Masses (RTFM) takes an alternative language approach, introducing tasks and named critical sections (via resources) natively in the RTFM-core language. RTFM-core programs can be compiled to native C-code, and efficiently executed onto single-core platforms under the Stack Resource Policy (SRP) by the RTFM-kernel. In this paper we formally define the well-formedness criteria for SRP based resource management, and develop a certified (formally proven) implementation of the corresponding compilation from nested critical sections of the input RTFM-core program to a resulting flat sequence of primitive operations and scheduling primitives. Moreover we formalise the properties for resource ceilings under SRP and develop a certified algorithm for their computation. The feasibility of the described approach is shown through the adoption of the Why3 platform, which allows the necessary verification conditions to be automatically generated and discharged through a variety of automatic external SMT-solvers and interactive theorem provers. Moreover, Why3 supports the extraction of certified Ocaml code for proven implementations in WhyML. As a proof of concept the certified extracted development is demonstrated on an example system.

Abstract

Abstract

Abstract
Multi-agent systems can play an important role in the realization of cyber-physical systems by providing intelligence, flexibility, robustness, self-adaptation, and self-organization to them. In spite of the promising perspective offered and concretized by the deployment of multi-agent systems in a few industrial systems and in several laboratory applications, its industrial adoption is far from the expected widely usage. Beside other issues, standardization is being identified as a critical aspect for this status and requires the need to be compliant with existing industrial practices but also a special effort to influence the specifications of existing standards and/or the introduction of new ones. The main objective of this paper is to analyze necessary standardization needs for applying and deploying agent-based technology in industrial environments, addressing industrial requirements imposed by different application fields.

Abstract
The increase of the use of Autonomous Vehicles in different types of environments leads to an improvement of the Localization and Navigation algorithms. The goal is to increase the levels of efficiency, security and robustness of the system, minimizing the tasks completion time. The application of cleaning robots in domestic environments have several advantages however some improvements should be performed in order to develop a robust system. Also in large spaces one robot doesn't achieve the desired performance in terms of robustness to faults and efficiency in the cleaning process. Considering a fleet of autonomous robots, this process could be improved. The purpose of our paper is the presentation of an architecture for management a fleet of cleaning robots, considering a complete coverage path planning for large and structured environments. Compartments are found in a grid-like decomposition and an area coverage strategy are evolved (optimized) by using Genetic Algorithms. The Task allocation module is based on Auctions strategy, thus obtaining cooperation under dynamic constraints in complex environments. The case study optimizes the number of robots involved in the cooperative cleaning of a full building in the campus, based on its real architectural plans.

Abstract
Joining efforts of academic and corporate teams, we developed an integration architecture - MULTIS - that enables corporate e-learning managers to use a Learning Management System (LMS) for management of educational activities in virtual worlds. This architecture was then implemented for the Formare LMS. In this paper we present this architecture and concretizations of its implementation for the Second Life Grid/OpenSimulator virtual world platforms. Current systems are focused on activities managed by individual trainers, rather than groups of trainers and large numbers of trainees: they focus on providing the LMS with information about educational activities taking place in a virtual world and/or being able to access within the virtual world some of the information stored in the LMS, and disregard the streamlining of activity setup and data collection in multi-trainer contexts, among other administrative issues. This architecture aims to overcome the limitations of existing systems for organizational management of corporate e-learning activities.