Abstract
Port authorities have the need to manage diverse information within the port area under its responsibility regarding their land and sea infrastructures. Through this innovation, which adds value to the port and its activity, it is made an interconnection of strategic areas, with the provision and sharing of structured data in a georeferenced environment. This work presents an innovative platform, based on various modules and allows effective control and efficient management of operations, processes and requirements associated with any sea port. The developed modules are designed to support the activities of business processes in the following areas of the port administration: Heritage, Hydrography, Port Traffic, Dominial, Studies and Works, Safety and Environment. Most of these modules were pioneers in the integration with business process management of portuguese ports of Leixoes and Viana do Castelo.

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. © 2016 IEEE.

Abstract
This paper considers a multi-item inventory distribution problem motivated by a practical case occurring in the logistic operations of an hospital. There, a single warehouse supplies several nursing wards. The goal is to define a weekly distribution plan of medical products that minimizes the visits to wards, while respecting inventory capacities and safety stock levels. A mathematical formulation is introduced and several improvements such as tightening constraints, valid inequalities and an extended reformulation are discussed. In order to deal with real size instances, an hybrid heuristic based on mathematical models is introduced and the improvements are discussed. A branch-and-cut algorithm using all the discussed improvements is proposed. Finally, a computational experimentation is reported to show the relevance of the model improvements and the quality of the heuristic scheme. © Springer International Publishing AG 2016.

Abstract

Abstract
This paper presents and evaluates a high-precision, one-way, and master-to-slave time synchronization protocol to minimize the clock time skew in low-power wearable sensor networks. The protocol is implemented in the media access control layer, and is based on directly eliminating deterministic delays during transmission from source to destination node, at hardware level. The proposed protocol keeps the one-hop average synchronization error close to the signal propagation delay, and the one-hop peak-to-peak jitter equals to the period of each node's system clock period. Both values grow linearly as the hop count increases. The protocol can achieve synchronization in the range of a few nanoseconds, enough to satisfy the requirements of many applications related to wearable networks, with one-way messages. Both theoretical analysis and experimental results, in wired wearable networks, show that the proposed protocol has a better performance than precision time protocol and a standard timing protocol for both single and multi-hop situations. The proposed approach is simpler, requires no calculations, and exchanges fewer messages. Experimental results obtained with an implementation of the protocol in a 0.35-mu m CMOS technology show that this approach keeps the one-hop average clock skew around 4.6 ns and peak-to-peak skew around 50 ns for a system clock frequency of 20 mh.

Abstract
This paper presents a novel approach on flexible and knowledge intensive process management, driven by a large automotive industry case study. The automotive company in analysis requires a very dynamic behaviour, based on high flexibility of both people and equipment. Market has been imposing a decreasing of automotive products life cycles, increasing the number of line adaptations during the entire value chain, resulting in an increased complexity from product design to production. To handle this complexity, new knowledge-based methods and technologies to model, simulate, optimize and monitor planned and existing manufacturing systems are required. Existing large Enterprise Information Systems impose totally structured and predictable workflow, while knowledge intensive processes are flexible and unpredictable, involving high amount of human-decision and interaction. This lead to the need of development of highly specialized applications. This paper presents a novel hybrid approach, including work, information and communication management, to support knowledge intensive processes. The application of the new solution in the automotive engineering process management proved to be very effective and efficient, leading to significant savings.