Web services are increasingly gaining acceptance as a framework for facilitating application-to-application interactions within and across enterprises. It is commonly accepted that a service description should include not only the interface, but also the business protocol supported by the service. The present work focuses on the formalization of the important category of protocols that include time-related constraints (called timed protocols), and the impact of time on compatibility and replaceability analysis. We formalized the following timing constraints: CInvoke constraints define time windows of availability while MInvoke constraints define expirations deadlines. We extended techniques for compatibility and replaceability analysis between timed protocols by using a semantic-preserving mapping between timed protocols and timed automata, leading to the novel class of protocol timed automata (PTA). Specifically, PTA exhibit silent transitions that cannot be removed in general, yet they are closed under complementation, making every type of compatibility or replaceability analysis decidable. Finally, we implemented our approach in the context of a larger project called ServiceMosaic, a model-driven framework for web service life-cycle management.

Embedded controllers coordinate the behaviours of specialised hardware components to satisfy broader application requirements. They are difficult to model and to program. One of the greatest challenges is to express intricate timing behaviours???which arise from the physical characteristics of components???while not precluding efficient implementations on resource-constrained platforms. Aspects of this challenge are addressed by this thesis through four distinct applications of timed automata and the synchronous languages Argos and Esterel. A novel framework for simulating controllers written in an imperative synchronous language is described. It includes a transformation of synchronous models into timed automata that accounts for timing properties which are important in constrained implementations but ignored by the usual assumption of synchrony. The transformation provides an interface between the discrete time of synchronous programs and a continuous model of time. This interface is extended to provide a way for simulating Argos programs within the widely-used Simulink software. Timed automata are well-suited for semantic descriptions, like the aforementioned transformation, and for modelling abstract algorithms and protocols. This thesis also includes a different type of case study. The timing diagram of a small-scale embedded component is modelled in more detail than usual with the aim of studying timing properties in this type of system. Multiple models are constructed, including one of an assembly language controller. Their interrelations are verified in Uppaal using a construction for timed trace inclusion testing. Existing constructions for testing timed trace inclusion do not directly address recent features of the Uppaal modelling language. Novel solutions for the problems presented by selection bindings, quantifiers, and channel arrays in Uppaal are presented in this thesis. The first known implementation of a tool for automatically generating a timed trace inclusion construction is described. The timed automata case study demonstrates one way of implementing application timing behaviours while respecting implementation constraints. A more challenging, but less detailed, example is proposed to evaluate the adequacy of Esterel for such tasks. Since none of the standard techniques are completely adequate, a novel alternative for expressing delays in physical time is proposed. Programs in standard Esterel are recovered through syntactic transformations that account for platform constraints.

Este trabalho consiste na proposição de uma metodologia que garanta o projeto efetivo de controladores para utilização em sistemas de proteção, operação e supervisão de sistemas APM (Automated People Movers), utilizando como estudo de caso o Sistema Aeromovel. Automated People Movers (APM) são sistemas de transporte de passageiros com operação completamente automatizada (sem tripulação), trafegando em vias exclusivas e com alta frequência de serviço. Geralmente são operados em via elevada, acima dos obstáculos encontrados no nível do solo, de maneira a manter o espaço urbano de circulação. A automação completa de trens para transporte de passageiros é geralmente condição essencial para sua viabilidade financeira nos casos onde tem-se veículos pequenos para prover alta frequência de serviço. Em parte, a confiabilidade de um veículo com operação completamente automatizada aumenta com o uso de vias exclusivas impedindo a interferência de outros veículos ou pessoas na via, porém, uma metodologia de desenvolvimento do sistema de proteção, operação e supervisão que diminua a taxa de falhas e suas consequências é necessária por tratar-se de um sistema crítico. Este trabalho apresenta uma revisão das soluções utilizadas na construção de Sistemas APM e daquelas adotadas no controle digital de sistemas automáticos. Descreve-se o processo de construção do sistema de proteção, operação e supervisão baseados na proposta de ampliação da norma IEC 61850 e prova-se a importância do uso do processo de simulação, verificação formal e os testes de conformidade no desenvolvimento de um sistema de controle seguro para aplicação em Sistemas APM. Para cada etapa do trabalho são apresentados os testes de conformidade para verificação do modelo de controle proposto. / This work consists in the proposition of a methodology that guarantees the effective design of controllers for use in protection, operation and monitoring Automated People Movers System, using as a case study Aeromovel system. Automated People Mover (APM) are systems of passenger transport with entirely automated operation (without crew), traveling in exclusive ways and with high service frequency. They are usually operated at elevated highway above the obstacles encountered on the ground level, so as to keep the urban space circulation. The complete automation of trains for passenger condition is necessary for their economic viability in the cases where they have small vehicles to supply high frequency of service. The reliability of an fully automated vehicle operation increases with the use of exclusive right-of-way preventing access from other vehicles or people on the track, however, the development of a methodology for protection, operation and monitoring systems is necessary to decrease the rate of failures and their consequences. This work presents a review of the solutions used in the construction of APM systems and the digital control of automated systems. We describe the construction process of the protection, operation and supervision systems based on the proposed extension of IEC 61850 and proves the importance use of the simulation, formal verification and conformity tests to develop a safe control system. For each stage of the work, the compliance tests to verify the proposed control model are presented.

Este trabalho consiste na proposição de uma metodologia que garanta o projeto efetivo de controladores para utilização em sistemas de proteção, operação e supervisão de sistemas APM (Automated People Movers), utilizando como estudo de caso o Sistema Aeromovel. Automated People Movers (APM) são sistemas de transporte de passageiros com operação completamente automatizada (sem tripulação), trafegando em vias exclusivas e com alta frequência de serviço. Geralmente são operados em via elevada, acima dos obstáculos encontrados no nível do solo, de maneira a manter o espaço urbano de circulação. A automação completa de trens para transporte de passageiros é geralmente condição essencial para sua viabilidade financeira nos casos onde tem-se veículos pequenos para prover alta frequência de serviço. Em parte, a confiabilidade de um veículo com operação completamente automatizada aumenta com o uso de vias exclusivas impedindo a interferência de outros veículos ou pessoas na via, porém, uma metodologia de desenvolvimento do sistema de proteção, operação e supervisão que diminua a taxa de falhas e suas consequências é necessária por tratar-se de um sistema crítico. Este trabalho apresenta uma revisão das soluções utilizadas na construção de Sistemas APM e daquelas adotadas no controle digital de sistemas automáticos. Descreve-se o processo de construção do sistema de proteção, operação e supervisão baseados na proposta de ampliação da norma IEC 61850 e prova-se a importância do uso do processo de simulação, verificação formal e os testes de conformidade no desenvolvimento de um sistema de controle seguro para aplicação em Sistemas APM. Para cada etapa do trabalho são apresentados os testes de conformidade para verificação do modelo de controle proposto. / This work consists in the proposition of a methodology that guarantees the effective design of controllers for use in protection, operation and monitoring Automated People Movers System, using as a case study Aeromovel system. Automated People Mover (APM) are systems of passenger transport with entirely automated operation (without crew), traveling in exclusive ways and with high service frequency. They are usually operated at elevated highway above the obstacles encountered on the ground level, so as to keep the urban space circulation. The complete automation of trains for passenger condition is necessary for their economic viability in the cases where they have small vehicles to supply high frequency of service. The reliability of an fully automated vehicle operation increases with the use of exclusive right-of-way preventing access from other vehicles or people on the track, however, the development of a methodology for protection, operation and monitoring systems is necessary to decrease the rate of failures and their consequences. This work presents a review of the solutions used in the construction of APM systems and the digital control of automated systems. We describe the construction process of the protection, operation and supervision systems based on the proposed extension of IEC 61850 and proves the importance use of the simulation, formal verification and conformity tests to develop a safe control system. For each stage of the work, the compliance tests to verify the proposed control model are presented.

Este trabalho consiste na proposição de uma metodologia que garanta o projeto efetivo de controladores para utilização em sistemas de proteção, operação e supervisão de sistemas APM (Automated People Movers), utilizando como estudo de caso o Sistema Aeromovel. Automated People Movers (APM) são sistemas de transporte de passageiros com operação completamente automatizada (sem tripulação), trafegando em vias exclusivas e com alta frequência de serviço. Geralmente são operados em via elevada, acima dos obstáculos encontrados no nível do solo, de maneira a manter o espaço urbano de circulação. A automação completa de trens para transporte de passageiros é geralmente condição essencial para sua viabilidade financeira nos casos onde tem-se veículos pequenos para prover alta frequência de serviço. Em parte, a confiabilidade de um veículo com operação completamente automatizada aumenta com o uso de vias exclusivas impedindo a interferência de outros veículos ou pessoas na via, porém, uma metodologia de desenvolvimento do sistema de proteção, operação e supervisão que diminua a taxa de falhas e suas consequências é necessária por tratar-se de um sistema crítico. Este trabalho apresenta uma revisão das soluções utilizadas na construção de Sistemas APM e daquelas adotadas no controle digital de sistemas automáticos. Descreve-se o processo de construção do sistema de proteção, operação e supervisão baseados na proposta de ampliação da norma IEC 61850 e prova-se a importância do uso do processo de simulação, verificação formal e os testes de conformidade no desenvolvimento de um sistema de controle seguro para aplicação em Sistemas APM. Para cada etapa do trabalho são apresentados os testes de conformidade para verificação do modelo de controle proposto. / This work consists in the proposition of a methodology that guarantees the effective design of controllers for use in protection, operation and monitoring Automated People Movers System, using as a case study Aeromovel system. Automated People Mover (APM) are systems of passenger transport with entirely automated operation (without crew), traveling in exclusive ways and with high service frequency. They are usually operated at elevated highway above the obstacles encountered on the ground level, so as to keep the urban space circulation. The complete automation of trains for passenger condition is necessary for their economic viability in the cases where they have small vehicles to supply high frequency of service. The reliability of an fully automated vehicle operation increases with the use of exclusive right-of-way preventing access from other vehicles or people on the track, however, the development of a methodology for protection, operation and monitoring systems is necessary to decrease the rate of failures and their consequences. This work presents a review of the solutions used in the construction of APM systems and the digital control of automated systems. We describe the construction process of the protection, operation and supervision systems based on the proposed extension of IEC 61850 and proves the importance use of the simulation, formal verification and conformity tests to develop a safe control system. For each stage of the work, the compliance tests to verify the proposed control model are presented.

Software testing is an important process for ensuring the quality of the software. As the complexity of the software increases, traditional means of manual testing becomes increasingly more complex and time consuming. In most embedded systems, designing software with as few errors as possible is often critical. Resource usage is also of concern for proper behavior because of the very nature of embedded systems.  To design reliable and energy-efficient systems, methods are needed to detect hot points of consumption and correct them prior to deployment. To reduce testing effort, Model-based testing can be used which is one testing method that allows for automatic testing of model based systems. Model-based testing has not been investigated extensively for revealing resource usage anomalies in embedded systems. UPPAAL SMC is a statistical model checking tool which can be used to model the system’s resource usage. Currently UPPAAL SMC lacks the support for performing automatic test generation and test selection. In this thesis we provide this support with a framework for automatic test generation and test selection using mutation analysis, a method for minimizing the generated test suite while maximizing the fault coverage and a tool implementing the framework on top of the UPPAAL SMC tool. The thesis also evaluates the framework on a Brake by Wire industrial system. Our results show that we could for a Brake-by-wire system, simulated on a consumer processor with five mutants, in best case find a test case that achieved 100% mutation score within one minute and confidently identify at least one test case that achieved full mutation score within five minutes. The evaluation shows that this framework is applicable and relatively efficient on an industrial system for reducing continues resource usage target testing effort.

Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems. PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified. This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems. The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy to handle and intuitive verification methods.

Event-triggered real-time systems are desirable to use in environments where the arrival of events are hard to predict. The semantics of an event-triggered system is well mapped to the behaviour of an active database management system (ADBMS), specified using event-condition-action (ECA) rules. The benefits of using an active database, such as persistent data storage, concurrency control, timely response to event occurrences etc. highlights the need for a development method for event-triggered real-time systems using active databases. However, there are problems left to be solved before an ADBMS can be used with confidence in real-time environments. The behaviour of a real-time system must be predictable, which implies a thorough analysed specification with e.g. specified worst case execution times. The predictability requirement is an obstacle for specifying real-time systems as ECA rules, since the rules may affect each other in many intricate ways which makes them hard to analyse. The interaction between the rules implies that it is not enough to verify the correctness of single rules; an analysis must consider the behaviour of the entire rule set. In this dissertation, an approach for developing active applications is presented. A method is examined which starts with an analysed high-level timed automaton specification and transforms the specified behaviour into an implicitly analysed rule set. For this method to be useful, the transformation from timed automata to rules must preserve the exact behaviour of the high level specification. Hence, the aim of this dissertation is to verify transformations between timed automaton specifications and ECA rules. The contribution of this project is a structured set of general transformations between timed automata specifications and ECA rules. The transformations include both transformations of small timed automata constructs for deterministic environments and formally verified timed automata patterns specifying the behaviour of composite events in recent and chronicle context.

Real-time systems are required to answer to external stimuli within a specified time-period. For this to be possible, the systems behaviour must be predictable. The use of active databases in real-time systems introduces unpredictability in the system, e.g. due to their use of active rules. The behaviour in active databases is usually specified in ECA-rules. Sets of ECA-rules are hard to analyse, which implies that the behaviour of the ECA-rule set is hard to predict. The purpose of this project is to evaluate the ability to support the development of a predictable ECA-rule set. Using a formal method for the specification task is desirable, since a formal specification is analysable and can be proven correct. In this project, timed-automata are used for specifying the systems behaviour. A method for deriving predictable ECA-rules from a timed-automaton specification is developed, and successfully applied on a case-study specification. For this case-study specification, a set of ECA-rules preserving the analysed behaviour of the timed-automata specification is derived.

Autonomous systems, or agents as they sometimes are called can be anything from drones, self-driving cars, or autonomous construction equipment. The systems are often given tasks of accomplishing missions in a group or more. This may require that they can work within the same area without colliding or disturbing other agents' tasks. There are several tools for planning and designing such systems, one of them being UPPAAL STRATEGO. Multi-agent planning (MAP) is about planning actions in optimal ways such that the agents can accomplish their mission efficiently. A method of doing this named MCRL, utilizes Q learning as the algorithm for  finding an optimal plan. These plans then need to be verified to ensure that they can accomplish what a user intended within the allowed time, something that UPPAAL STRATEGO can do. This is because a Q-learning algorithm does not have a correctness guarantee. Using this method alleviates the state-explosion problem that exists with an increasing number of agents. Using UPPAAL STRATEGO it is also possible to acquire the best and worst-case execution time (BCET and WCET) and their corresponding traces. This thesis aims to obtain the BCET and WCET and their corresponding traces in the model.