Linear Temporal Logic (LTL) can be used for problem-solving when all problem constraints can be specified in this logic through the use of satisfiability checking techniques. In optimization problems such as scheduling with preferences, where constraints are primarily temporal, LTL is a desirable specification formalism. However, LTL cannot be used as a standalone formalism due to the fact that it is unable to specify soft constraints. This article introduces Optimization LTL (OLTL), an optimization-oriented extension of LTL that can specify both hard and soft constraints in optimization problems. The syntax, semantics and basic formal properties of this logic are presented, along with an encoding based on bit-vector logic and Linear Real Arithmetic (LRA). Additionally, a tool called LiTeLLab ( Li near Te mporal L ogic Lab oratory) is introduced to solve optimization problems specified by OLTL. The feasibility and scalability of using OLTL as a specification formalism is demonstrated through two case studies. These problems, with multiple optimization parameters, are specified in OLTL and LiTeLLab successfully generates optimal solutions.

Osteoarthritis is a degenerative condition that affects bones and cartilage, often leading to structural changes, including osteophyte formation, bone density loss, and the narrowing of joint spaces. Over time, this process may disrupt the glenohumeral (GH) joint functionality, requiring a targeted treatment. Various options are available to restore joint functions, ranging from conservative management to surgical interventions, depending on the severity of the condition. This work introduces an innovative deep learning framework to process shoulder CT scans. It features the semantic segmentation of the proximal humerus and scapula, the 3D reconstruction of bone surfaces, the identification of the GH joint region, and the staging of three common osteoarthritic-related conditions: osteophyte formation (OS), GH space reduction (JS), and humeroscapular alignment (HSA). Each condition was stratified into multiple severity stages, offering a comprehensive analysis of shoulder bone structure pathology. The pipeline comprised two cascaded CNN architectures: 3D CEL-UNet for segmentation and 3D Arthro-Net for threefold classification. A retrospective dataset of 571 CT scans featuring patients with various degrees of GH osteoarthritic-related pathologies was used to train, validate, and test the pipeline. Root mean squared error and Hausdorff distance median values for 3D reconstruction were 0.22 mm and 1.48 mm for the humerus and 0.24 mm and 1.48 mm for the scapula, outperforming state-of-the-art architectures and making it potentially suitable for a PSI-based shoulder arthroplasty preoperative plan context. The classification accuracy for OS, JS, and HSA consistently reached around 90% across all three categories. The computational time for the entire inference pipeline was less than 15 s, showcasing the framework's efficiency and compatibility with orthopedic radiology practice. The achieved reconstruction and classification accuracy, combined with the rapid processing time, represent a promising advancement towards the medical translation of artificial intelligence tools. This progress aims to streamline the preoperative planning pipeline, delivering high-quality bone surfaces and supporting surgeons in selecting the most suitable surgical approach according to the unique patient joint conditions.

The paper addresses the problem of estimating the energy consumed by production resources in manufacturing so that alternative process designs can be compared in terms of energy expenditure. In particular, the proposed methodology focuses on Computer Numerical Controlled (CNC) machining centers. Classical approaches to energy modeling require high expertise and large development effort since, for example, data acquisition is resource-specific and must be repeated frequently to avoid obsolescence. An automated and flexible data-driven methodology is designed in this work. A data-driven method is employed to learn a hybrid and stochastic model of a CNC machining center’s energetic behavior. The learned model is used to provide offline energy consumption estimates of simulated part-programs before the actual execution of the cutting. Numerical results show the performance of the proposed method on a set of case studies. The methodology is also applied to a real industrial application, including data collected during machine production.Note to Practitioners—This article provides a flexible and autonomous data-driven approach to building models representing the energetic behavior of production resources, particularly CNC machining centers. The learned models can predict machine energy consumption while executing complex part-programs. The algorithm uses data that are commonly acquired by contemporary machine monitoring systems and does not require ad-hoc experimental tests for training. Specifically, it requires the spindle rotary speed signal, part load/unload signal, and spindle (or machine) power signal during the learning phase, whilst the estimation phase uses only the load/unload and spindle speed simulated signals.

Abstract Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a critical source of uncertainty for the outcome of the robotic mission. Application designers require accessible and reliable frameworks to address this issue at an early development stage. We present a model-driven framework for developing interactive service robotic scenarios, allowing designers to model the interactive scenario, estimate its outcome, deploy the application, and smoothly reconfigure it. This article extends the framework compared to previous works by introducing an analysis of the impact of human errors on the mission’s outcome. The core of the framework is a formal model of the agents at play—the humans and the robots—and the robotic mission under analysis, which is subject to statistical model checking to estimate the mission’s outcome. The formal model incorporates a formalization of different human erroneous behaviors’ phenotypes, whose likelihood can be tuned while configuring the scenario. Through scenarios inspired by the healthcare setting, the evaluation highlights how different configurations of erroneous behavior impact the verification results and guide the designer toward the mission design that best suits their needs.

Abstract Interoperability stands as a critical hurdle in developing and overseeing distributed and collaborative systems. Thus, it becomes imperative to gain a deep comprehension of the primary obstacles hindering interoperability and the essential criteria that systems must satisfy to achieve it. In light of this objective, in the initial phase of this research, we conducted a survey questionnaire involving stakeholders and practitioners engaged in distributed and collaborative systems. This effort resulted in the identification of eight essential interoperability requirements, along with their corresponding challenges. Then, the second part of our study encompassed a critical review of the literature to assess the effectiveness of prevailing conceptual approaches and associated technologies in addressing the identified requirements. This analysis led to the identification of a set of components that promise to deliver the desired interoperability by addressing the requirements identified earlier. These elements subsequently form the foundation for the third part of our study, a reference architecture for interoperability-fostering frameworks that is proposed in this paper. The results of our research can significantly impact the software engineering of interoperable systems by introducing their fundamental requirements and the best practices to address them, but also by identifying the key elements of a framework facilitating interoperability in Systems of Systems.

Evidence is rapidly accumulating that multifactorial nocturnal monitoring, through the coupling of wearable devices and deep learning, may be disruptive for early diagnosis and assessment of sleep disorders. In this work, optical, differential air-pressure and acceleration signals, acquired by a chest-worn sensor, are elaborated into five somnographic-like signals, which are then used to feed a deep network. This addresses a three-fold classification problem to predict the overall signal quality (normal, corrupted), three breathing-related patterns (normal, apnea, irregular) and three sleep-related patterns (normal, snoring, noise). In order to promote explainability, the developed architecture generates additional information in the form of qualitative (saliency maps) and quantitative (confidence indices) data, which helps to improve the interpretation of the predictions. Twenty healthy subjects enrolled in this study were monitored overnight for approximately ten hours during sleep. Somnographic-like signals were manually labeled according to the three class sets to build the training dataset. Both record- and subject-wise analyses were performed to evaluate the prediction performance and the coherence of the results. The network was accurate (0.96) in distinguishing normal from corrupted signals. Breathing patterns were predicted with higher accuracy (0.93) than sleep patterns (0.76). The prediction of irregular breathing was less accurate (0.88) than that of apnea (0.97). In the sleep pattern set, the distinction between snoring (0.73) and noise events (0.61) was less effective. The confidence index associated with the prediction allowed us to elucidate ambiguous predictions better. The saliency map analysis provided useful insights to relate predictions to the input signal content. While preliminary, this work supported the recent perspective on the use of deep learning to detect particular sleep events in multiple somnographic signals, thus representing a step towards bringing the use of AI-based tools for sleep disorder detection incrementally closer to clinical translation.

This paper studies how bit-vector logic (bv logic) can help improve the efficiency of verifying specifications expressed in Linear Temporal Logic (LTL). First, it exploits the notion of Bounded Satisfiability Checking to propose an improved encoding of LTL formulae into formulae of bv logic, which can be formally verified by means of Satisfiability Modulo Theories (SMT) solvers. To assess the gain in efficiency, we compare the proposed encoding, implemented in our tool$\mathbb {Z}$ot, against three well-known encodings available in the literature: the classic bounded encoding and the optimized, incremental one, as implemented in both NuSMV and nuXmv, and the encoding optimized for metric temporal logic, which was the “standard” implementation provided by$\mathbb {Z}$ot. We also compared the newly proposed solution against five additional efficient algorithms proposed by nuXmv, which is the state-of-the-art tool for verifying LTL specifications. The experiments show that the new encoding provides significant benefits with respect to existing tools. Since the first set of experiments only used Z3 as SMT solver, we also wanted to assess whether the benefits were induced by the specific solver or were more general. This is why we also embedded different SMT solvers in$\mathbb {Z}$ot. Besides Z3, we also carried out experiments with CVC4, Mathsat, Yices2, and Boolector, and compared the results against the first and second best solutions provided by either NuSMV or nuXmv. Obtained results witness that the benefits of the bv logic encoding are independent of the specific solver. Bv logic-based solutions are better than traditional ones with only a few exceptions. It is also true that there is no particular SMT solver that outperformed the others. Boolector is often the best as for memory usage, while Yices2 and Z3 are often the fastest ones.

Graph data structures model relations between entities in various domains. Graph processing systems enable scalable distributed computations over large graphs, but are limited to static scenarios in which the structure of the graph does not change. However, many applications are dynamic in nature, and this reflects to graphs that continuously evolve over time. In these contexts, understanding the evolution of graphs is key to enable timely reactions when necessary. We address this problem by proposing a new model to express temporal patterns over graph data structures. The model seamlessly integrates computations over graphs to extract relevant values, and temporal operators that define patterns of interest in the evolution of the graph. We present the syntax and semantics of our model and discuss its concrete implementation in FlowGraph, a middleware for temporal pattern recognition in large scale graphs. FlowGraph presents a level of performance that is comparable to state-of-the-art graph processing tools when processing static graphs. In the presence of temporal patterns, it can further optimize processing by avoiding complex graph computations until strictly necessary for pattern evaluation.

The ability to perform automated conversions between data conforming to different specifications is a key ingredient to achieve interoperability among heterogeneous systemswhich, in turn, is at the basis of the creation of so-called Systems of Systems.These conversions require the definition of mappings between concepts of separate data specifications, which is typically a hard and time-consuming task.In this paper, we present a technique to automatically suggest mappings to users, based on both linguistic and structural similarities between terms.The approach has been implemented in our prototype tool, SMART (SPRINT Mapping & Annotation Recommendation Tool), and it has been validated through tests carried out using specifications from the transportation domain.

Robots are currently mostly found in industrial settings. In the future, a wider range of environments will benefit from their inclusion. This calls for the development of tools that allow professionals to set up dependable robotic applications in which people productively interact with robots aware of their needs. Given the co-existence of humans and robots, the precise analysis-e.g., through formal verification techniques-of properties related to aspects such as human needs and physiology is of paramount importance. In this paper, we present a formally-based, model-driven approach to design and verify scenarios involving human-robot interactions. Some of the features of our approach are tailored to the healthcare domain, from which our case studies are derived. In our approach, the designer specifies the main parameters of the mission to generate the model of the application, which includes mobile robots, the humans to be served, including some of their physiological features, and the decision-maker that orchestrates the execution. All components are modeled through hybrid automata to capture variables with complex dynamics. The model is verified through Statistical Model Checking (SMC), using the Uppaal tool, to determine the probability of success of the mission. The results are examined by the developer, who iteratively refines the design until the probability of success is satisfactory.

Abstract Apache Spark is probably the most widely adopted framework for developing big-data batch applications and for executing them on a cluster of (virtual) machines. In general, the more resources (machines) one uses, the faster applications execute, but there is currently no adequate means to determine the proper size of a Spark cluster given time constraints, or to foresee execution times given the number of employed machines. One can only run these applications and use her/his experience to size the cluster and predict expected execution times. Wrong estimation of execution times can lead to costly overruns and overly long executions, thus calling for analytic sizing/prediction techniques that provide precise time guarantees. This paper addresses this problem by proposing a solution based on model-checking. The approach exploits a directed acyclic graph (DAG) to abstract the structure of the execution flows of Spark programs, annotates each node (Spark stage) with execution-related data, and formulates the identification of the global execution time as a reachability problem. To avoid the well-known state space explosion problem, the paper also proposes a technique to reduce the size of generated abstract models. This results in a significant decrease in used memory and/or verification time making our approach feasible for predicting the execution time of Spark applications given the resources available. The benefits of the proposed reduction technique are evaluated by using both timed automata and constraint LTL over clocks logic to formally encode and analyze generated models. The approach is also successfully validated on some realistic case studies. Since the optimization is not Spark-specific, we claim that it can be applied to a wide range of applications whose underlying model can be abstracted as a DAG.

Abstract Developing robotic applications is a complex task, which requires skills that are usually only possessed by highly-qualified robotic developers. While formal methods that help developers in the creation and design of robotic applications exist, they must be explicitly customized to be impactful in the robotics domain and to support effectively the growth of the robotic market. Specifically, the robotic market is asking for techniques that: (i) enable a systematic and rigorous design of robotic applications though high-level languages; and (ii) enable the automatic synthesis of low-level controllers, which allow robots to achieve their missions. To address these problems we present the PuRSUE (Planner for RobotS in Uncontrollable Environments) approach, which aims to support developers in the rigorous and systematic design of high-level run-time control strategies for robotic applications. The approach includes PuRSUE-ML a high-level language that allows for modeling the environment, the agents deployed therein, and their missions. PuRSUE is able to check automatically whether a controller that allows robots to achieve their missions might exist and, then, it synthesizes a controller. We evaluated how PuRSUE helps designers in modeling robotic applications, the effectiveness of its automatic computation of controllers, and how the approach supports the deployment of controllers on actual robots. The evaluation is based on 13 scenarios derived from 3 different robotic applications presented in the literature. The results show that: (i) PuRSUE-ML is effective in supporting designers in the formal modeling of robotic applications compared to a direct encoding of robotic applications in low-level modeling formalisms; (ii) PuRSUE enables the automatic generation of controllers that are difficult to create manually; and (iii) the plans generated with PuRSUE are indeed effective when deployed on actual robots.

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified, which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts. This article presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula, which is verified through an available decision procedure. The technique is flexible, since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.

A crucial aspect of physical human-robot collaboration (HRC) is to maintain a safe common workspace for human operator. However, close proximity between human-robot and unpredictability of human behavior raises serious challenges in terms of safety. This article proposes a risk analysis methodology for collaborative robotic applications, which is compatible with well-known standards in the area and relies on formal verification techniques to automate the traditional risk analysis methods. In particular, the methodology relies on temporal logic-based models to describe the different possible ways in which tasks can be carried out, and on fully automated formal verification techniques to explore the corresponding state space to detect and modify the hazardous situations at early stages of system design.

We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.

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.

Linear Temporal Logic (LTL) has been used in computer science for decades to formally specify programs, systems, desired properties, and relevant behaviors. This paper presents a novel, efficient technique for verifying LTL specifications in a fully automated way. Our technique belongs to the category of Bounded Satisfiability Checking approaches, where LTL formulae are encoded as formulae of another decidable logic that can be solved through modern satisfiability solvers. The target logic in our approach is Bit-Vector Logic. We present our novel encoding, show its correctness, and experimentally compare it against existing encodings implemented in well-known formal verification tools.

Model-driven engineering (MDE) often features quality assurance (QA) techniques to help developers creating software that meets reliability, efficiency, and safety requirements. In this paper, we consider the question of how quality-aware MDE should support data-intensive software systems. This is a difficult challenge, since existing models and QA techniques largely ignore properties of data such as volumes, velocities, or data location. Furthermore, QA requires the ability to characterize the behavior of technologies such as Hadoop/MapReduce, NoSQL, and stream-based processing, which are poorly understood from a modeling standpoint. To foster a community response to these challenges, we present the research agenda of DICE, a quality-aware MDE methodology for data-intensive cloud applications. DICE aims at developing a quality engineering tool chain offering simulation, verification, and architectural optimization for Big Data applications. We overview some key challenges involved in developing these tools and the underpinning models.

Constraint LTL-over-clocks is a variant of CLTL, an extension of linear-time temporal logic allowing atomic assertions in a concrete constraint system. Satisfiability of CLTL-over-clocks is here shown to be decidable by means of a reduction to a decidable SMT (Satisfiability Modulo Theories) problem. The result is a complete Bounded Satisfiability Checking procedure, which has been implemented by using standard SMT solvers. The importance of this technique derives from the possibility of translating various continuous-time metric temporal logics, such as MITL and QTL, into CLTL-over-clocks itself. Although standard decision procedures of these logics do exist, they have never been realized in practice. Suitable translations into CLTL-over-clocks have instead allowed us the development of the first prototype tool for deciding MITL and QTL. The paper also reports preliminary, but encouraging, experiments on some significant examples of MITL and QTL formulae.

The design of complex embedded software systems requires the careful analysis of the system and of the environment it interacts with. The different natures of these two elements are difficult to address by means of a single all-encompassing technique/notation. The paper proposes MCA, the MADES Co-simulation Approach, which allows designers to combine different, complementary formalisms in a seamless manner: the system is rendered through logic formulae, while the environment is demanded to Modelica. These two models are input to MCA to produce an execution trace that is “compatible” with them, that is, that does not violate either model. The paper introduces the theoretical basis of MCA and exemplifies it on a case study.

Many industrial systems include components interacting with each other that evolve with possibly very different speeds. To deal with this situation many formalisms adopt the abstraction of ``zero-time transitions'', which do not consume time. These, however, have several drawbacks in terms of naturalness and logic consistency, as a system is modeled to be in different states at the same time. We introduce a metric temporal logic, called X-TRIO, that uses non-standard analysis to elegantly deal with zero-time transitions in an abstract, descriptive way. We study the decidability of the logic, and we introduce a decision procedure for a subset thereof. X-TRIO has been applied in companion works to the design and verification of industrial systems.

SCORE 2011 is the second iteration of a team-oriented software engineering contest that attracts student teams from around the world, culminating in a final round of competition and awards at ICSE. Each team has responded to one of the project proposals provided by the SCORE program committee, usually in the context of a software engineering project course. In this second iteration we have built on the success of SCORE 2009, greatly expanding the number and geographical distribution of student teams, including many of very high quality.

When dependability of systems with a large number of components is a concern, being able to model and analyze their properties, especially non-functional ones, in a formal and automated way becomes essential. Often, however, the application of formal methods and automated reasoning is seen by practitioners as complex and time consuming. Compositional techniques can help modify this belief. In this paper we show how a compositional modeling and verification technique can be applied to the analysis of distributed systems with numerous interacting nodes. We automate the proof by exploiting a SAT-based tool. We demonstrate the validity of the resulting approach by applying it to an autonomic service-based system that manages, in a coordinated peer-to-peer manner, electricity consumption in a geographical area. In particular, we show that in this case the time needed for performing the proof is remarkably shorter than in the case in which we adopt a non-compositional approach.

An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, to avoid that the check may affect the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a formal verification technique for an extension of Linear Temporal Logic that allows users to include in formulae constraints on integer variables. This technique applied to the substitutability problem for conversational services is shown to be considerably faster and with smaller memory footprint than existing ones.

This paper defines CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. The paper introduces suitable restrictions and assumptions that make the satisfiability problem decidable in many cases, although the problem is undecidable in the general case. Decidability is shown for a large class of constraint systems, and an encoding into Boolean logic is defined. This paves the way for applying existing SMT-solvers for checking the Bounded Reachability problem, as shown by various experimental results.

This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to “flat” formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete time, resulting in an automated partial practically efficient discretization technique.

A core problem in formal methods is the transition from informal requirements to formal specifications. Especially when specifying reactive systems, many formalisms require the user to either understand a complex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. While formalizing a real-world requirements document, we developed a technique where not states but signal patterns are the main elements. We argue that it supports a formalization that is often closer to the informal requirements and thus provides a smoother transition to formal methods. As only tables of regular expressions are used for notation, the technique can easily be understood by non-mathematicians. Many properties, such as consistency, can be checked automatically on these specifications. Besides the formal foundation of our approach, this paper presents prototypical tool support and first results from an industrial case study.

In this paper we argue that the modeling activity in the development of software-intensive systems should formalize as much as possible of the environment in which the application being developed operates. We also show that a rich formal model of the environment helps developers clearly state requirements that might typically be considered intrinsically informal (or non- formalizable in general). To illustrate this point, we show how a requirement for "orderly safe traffic" in a traffic system can be modeled, and we briefly discuss the benefits thereof.

The paper "An Interval Logic for Real-Time System Specification" (Mattolini and Nesi, IEEE Trans. Software Eng., vol. 27, no. 3, pp. 208-227, Mar. 2001) presents the TILCO specification language and compares it to other existing similar languages. In this comment, we show that several of the logic formulas used for the comparison are flawed and/or overly complicated and we explain why, in this respect, the comparison is moot

We introduce a formal model for describing Real-Time CORBA-based applications, and a set of guidelines to formally check that the design of such an application is consistent with its specification. The model and the guidelines are then applied to the verification of a simple test application.

The design of distributed applications in a CORBA-based environment can be carried out by means of an incremental approach, which starts from the specification and leads to the high-level architectural design. This article discusses a methodology to transform a formal specification written in TRIO into a high-level design document written in an extension of TRIO, named TRIO/CORBA (TC). The TC language is suited to formally describe the high-level architecture of a CORBA-based application. As a result, designers are offered high-level concepts that precisely define the architectural elements of an application. Furthermore, TC offers mechanisms to extend its base semantics, and can be adapted to future developments and enhancements in the CORBA standard. The methodology and the associated language are presented through a case study derived from a real Supervision and Control System.

The design of distributed applications in a CORBA based environment can be carried out by means of an incremental approach, which starts from the specification and leads to the high level architectural design. This is done by introducing in the specification all typical elements of CORBA and by providing a methodological support to the designers. The paper discusses a methodology to transform a formal specification written in TRIO into a high level design document written using an extension of TRIO named TC. The TC language is suited to formally describe the high level architecture of a CORBA based application. The methodology and the associated language are presented by means of an example involving a real Supervision and Control System.