Service-oriented systems have recently emerged as context-independent component-based systems. Unlike components, services can be created, invoked, composed, and destroyed at run-time. Consequently, all services should have a way of advertising their capabilities to the entities that will use them, and service-oriented modeling should cater for various kinds of service composition. In this paper, we show how services can be formally described by the resource-aware timed behavioral language REMES, which we extend with service-specific information, such as type, capacity, time-to-serve, etc., as well as boolean constraints on inputs, and output guarantees. Assuming a Hoare-triple model of service correctness, we show how to check it by using the strongest postcondition semantics. To provide means for connecting REMES services, we propose a hierarchical language for service composition, which allows for verifying the latter’s correctness. The approach is applied on an abstracted version of an intelligent shuttle system, for which we also compute resource-efficient behaviors, and energy-time trade-offs, by model-checking the system’s underlying Priced Timed Automata semantic representation.

Programmable logic controllers (PLCs), as a specialized type of embedded systems, have been introduced to increase system flexibility and reliability, but at the same time to give faster response time and lower cost of implementation. In the beginning, their use brought a revolutionary change, but with the constant growth of system complexity, it became harder to guarantee both functional and extra functional properties, as early as possible in the development process. In this paper, we show how formal methods can be applied to describe PLC-based systems and illustrate it on an example of a car wash system. First, we show how the existing behavioral modeling language REMES (resource model for embedded systems) can be extended to model the behavior of such systems. Second, we show how Remes can be translated into networks of timed automata and priced timed automata in order to support safety and resource-wise reasoning about PLC systems. The formal verification of PLC systems is carried out in the Uppaal and Uppaal Cora tools.

There is no clear distinction between service-oriented systems (SOS) and component-based systems (CBS). However, there are several characteristics that could let one consider SOS as a step further from CBS. In this paper, we discuss the general features of CBS and SOS, while accounting for behavioral modeling in the language called REMES. First, we present REMES in the context of CBS modeling, and then we show how it can become suitable for SOS. We also discuss the relation between our model and the current state of the art.

This document is a revised version of Deliverable D3.1 and includes the description of prediction models which support the estimate of the quality attributes considered in the Q-ImPrESS project. Models are discussed within the Model Driven Development framework and their points of strength and weakness are analyzed. An example of use of the models with respect to the clientserver architecture introduced in Q-ImPrESS Deliverable D2.1 is also provided and the interrelationships among the model parameters and the Q-ImPrESS Service Architecture Meta-Model is analyzed. Furthermore, the document describes the selection of prediction models used in Q-ImPrESS project for performance and reliability estimates and presents an original approach for the evaluation of maintainability property. c © Q-ImPrESS Consortium Dissemination Level: public Page 2/75 D3.1: Prediction Models Specification (revised version) Version: 2.0 Last change: September 15, 2009

An early prediction of resource utilization and its impact on system performance and reliability can reduce the overall system cost, by allowing early correction of detected problems, or changes in development plans with minimized overhead. Nowadays, researchers are using both academic and commercial models to predict such attributes, by measuring them at earliest stages of system development. In this paper, we give a short overview of existing prediction models for performance and reliability, targeting popular component-based frameworks. Next, we describe our own approach for tackling such predictions, through an illustration on a small example that deals with estimations of energy consumption.

This document introduces and describes the prediction models which support the estimate of the quality attributes considered in the Q-ImPrESS project. Models are discussed within the Model Driven Development frame- work and their points of strength and weakness are analyzed. An example of use of the models with respect to the client-server architecture introduced in Q-ImPrESS Deliverable D2.1 is also provided and the interrelationships among the model parameters and the Q-ImPrESS Service Architecture Meta-Model is analyzed.