This article presents a novel technique to formally verify models of real-time systems captured through a set of heterogeneous UML diagrams. The technique is based on the following key elements: (i) a subset of Unified Modeling Language (UML) diagrams, called Coretto UML (C-UML), which allows designers to describe the components of the system and their behavior through several kinds of diagrams (e.g., state machine diagrams, sequence diagrams, activity diagrams, interaction overview diagrams), and stereotypes taken from the UML Profile for Modeling and Analysis of Real-Time and Embedded Systems; (ii) a formal semantics of C-UML diagrams, defined through formulae of the metric temporal logic Tempo Reale ImplicitO (TRIO); and (iii) a tool, called Corretto, which implements the aforementioned semantics and allows users to carry out formal verification tasks on modeled systems. We validate the feasibility of our approach through a set of different case studies, taken from both the academic and the industrial domain.

Summary Modern software systems are increasingly built by integrating different services implemented by independent organizations and offered in an open service marketplace. In such environment, multiple providers may compete with each other by publishing services that provide the same functionality, and export the same interface, but differ in the offered QoS and in particular in the offered performance. Clients and service integrators may therefore dynamically select the most efficient services that satisfy their requirements among the competing alternatives. Service selection may be performed by clients by following different strategies, which may ultimately affect the overall quality of service invocations. In this paper, we address the problem of analyzing and comparing different service selection strategies based on a framework that supports performance estimates. We report on quantitative analyses through simulations, highlighting advantages and limitations of each strategy. Copyright © 2014 John Wiley & Sons, Ltd.

While many software design tools exist and are in use daily, when faced with a design problem, developers will more often then not turn to the whiteboard to work on potential solutions. It has been observed that the sketches that software engineers create in this process transition from quite informal, rough sketches to sketches that reflect design notations like UML diagrams or user interfaces with quite precise layout and content. This behavior leads to an interesting opportunity: what if, during this refinement phase, it becomes possible for a whiteboard sketching tool to insert lightweight analyses that provide the developer with feedback about their design at hand? This paper investigates this opportunity, particularly focusing on exploring whether it might be possible to add a lightweight analysis and feedback mechanism to one sketching tool, Calico, that gives the designer insight into the perceived performance of their application.

UML is a general-purpose modeling language that offers a heterogeneous set of diagrams to describe the different views of a software system. While there seems to be a general consensus on the semantics of some individual diagrams, the composite semantics of the different views is still an open problem. During my PhD I am considering a significant and consistent set of UML diagrams, where timed-related properties can be modeled carefully, and I am ascribing them with a formal semantics based on metric temporal logic. The use of logic is aimed to help capture the composite semantics of the different views efficiently. The result is then used to feed a bounded model/satisfiability checker to allow users to verify these systems, even from the initial phases of the design. The final goal is to realize an advanced modeling framework where users can exploit both a well-known modeling notation and advanced verification capabilities seamlessly.