Modern embedded systems are evolving in the direction of increased adaptivity and complexity. It is extremely important for a system with limited resource to be adaptive in order to maximize its efficiency of resource usage while guaranteeing a high level of fault tolerance and QoS. This report aims at exploring such a kind of system, i.e. Adaptive Embedded System (AES), which is featured by dynamic reconfiguration at runtime. Based on the investigation and analysis of a variety of case studies related with AES, we proposed the conceptual view and overall architecture of an AES by highlighting its predominant characteristics. We also made an incomplete but detailed summary of the most popular techniques that can be used to realize adaptivity. Those techniques are categorized into dynamic CPU/network resource re-allocation and adaptive fault tolerance. A majority of adaptive applications resort to one or more of those techniques. Besides, there is a separate discussion on dynamic reconfiguration and mode switch for AES. Finally, we classify adaptivity into different modeling problems at a higher abstraction level and build UPPAAL models for two different AESs, a smart phone and an object-tracking robot. Our UPPAAL models provide clear demonstration on how a typical AES works.

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.

Master of Science / Department of Computing and Information Sciences / Mitchell L. Neilsen / Safety-critical systems embedded in avionics and automotive systems are becoming increasing complex. Components with different requirements typically share a common distributed platform for communication. To accommodate varied requirements, many of these distributed real-time systems use FlexRay communication network. FlexRay supports both time triggered and event-triggered communications. In such systems, it is vital to establish a consistent view of all the associated processes to handle fault-tolerance. This task can be accomplished through the use of a Process Group Membership Protocol. This protocol must provide a high level of assurance that it operates correctly. In this thesis, we provide for the verification of one such protocol using Model Checking. Through this verification, we found that the protocol may remove nodes from the group of operational nodes in the communicating network at a fast rate. This may lead to exhaustion of the system resources by the protocol, hampering system performance. We determine allowable rates of failure that do not hamper system performance.

Dans cette thèse nous nous sommes intéressés aux problèmes concernant la conception et la gestion des plans de soins à domicile. Un plan de soins à domicile définit l'ensemble des activités médicales et/ou sociales qui sont menées jour après jour au domicile d'un patient. Ce plan de soins est généralement construit à travers un processus complexe impliquant une évaluation complète des besoins du patient ainsi que son environnement social et physique. La spécification de plans de soins à domicile est difficile pour plusieurs raisons: les plans de soins à domicile sont par nature des processus non structurés qui impliquent des activités répétitives mais irrégulières, dont la spécification requiert des expressions temporelles complexes. Ces caractéristiques font que les plans de soins à domicile sont difficiles à modéliser en utilisant les technologies traditionnelles de modélisation de processus. Tout d'abord, nous présentons l'approche basée sur les DSL (Langage spécifique au domaine) qui permet d'exprimer les plans de soins à domicile en utilisant des abstractions de haut niveau et orientées utilisateur. Le DSL nous permet à travers cette thèse de proposer un langage de temporalités permettant de spécifier les temporalités des activités du plan de soins à domicile. Ensuite, nous décrivons comment les plans de soins à domicile, formalisés grâce aux automates temporisés, peuvent être générés à partir de ces abstractions. Nous proposons une approche en trois étapes qui consiste à: (i) le mapping entre les spécifications temporelles élémentaires et les automates temporisés appelés "pattern automata", (ii) la combinaison des "patterns automata" afin de construire les automates d'activités en utilisant l'algorithme de composition que nous avons déni, et aussi (iii) la construction de l'automate de plan de soins à domicile global. L'automate de plan de soins à domicile résultant englobe tous les schedules autorisés des activités pour un patient donné. Enfin, nous montrons comment la vérification et le suivi de l'automate du plan de soins à domicile résultant peuvent être faits en utilisant des techniques et des outils existants, en particulier en utilisant l'outil de verification UPPAAL. / In this thesis we are interested in the problems underlying the design and the management of home care plans. A home care plan defines the set of medical and/or social activities that are carried out day after day at a patient's home. Such a care plan is usually constructed through a complex process involving a comprehensive assessment of patient's needs as well as his/her social and physical environment. Specication of home care plans is challenging for several reasons: home care plans are inherently nonstructured processes which involve repetitive, but irregular, activities, whose specification requires complex temporal expressions. These features make home care plans difficult to model using traditional process modeling technologies. First, we present a DSL (Domain Specific Language) based approach tailored to express home care plans using high level and user-oriented abstractions. DSL enables us through this thesis to propose a temporalities language to specify temporalities of home care plan activities. Then, we describe how home care plans, formalized as timed automata, can be generated from these abstractions. We propose a three-step approach which consists in (i) mapping between elementary temporal specifications and timed automata called Pattern automata, (ii) combining patterns automata to build the activity automata using our composition algorithm and then (iii) constructing the global care plan automaton. The resulting care plan automaton encompasses all the possible allowed schedules of activities for a given patient. Finally, we show how verification and monitoring of the resulting care plan can be handled using existing techniques and tools, especially using UPPAAL Model Checker.

Safety-critical systems require high quality and dependability levels, where system correctness and safety are major features to avoid any severe outcome. Time and cost are also important challenges that are imposed during the development process. Describing the behavior of a system in a high level provides a realistic vision and anticipation of the system. This presents a valuable opportunity for verifying the system before wasting the intended resources to develop the system. Architecture Description Languages (ADLs) provide the ability to comprise and represent the system level details of components, interactions and configuration. Architecture Analysis and Design Language (AADL) as a family member of ADLs proved its effectiveness in designing software intensive systems. In this report, we present a case study to validate “An Architecture-Based Verification Technique for AADL Specifications”. The technique involves a combination of model checking and model-based testing approaches adapted to an architectural perspective. The objectives of the verification process are 1) to ensure completeness and consistency of an AADL specification, and 2) to ensure conformance of an implementation with respect to its AADL specification. The technique has only been applied to small examples, and the goal of this thesis work is to validate it against a safety-critical system developed by a major vehicle manufacturer. Validation of the technique begins by investigating the system and specifying it in AADL. The defined verification criteria are subsequently applied to the AADL specification which drives the verification process. The case study presents interesting results while performing the model checking (the completeness and consistency checking). Conformance testing, on the other hand, could not be performed on the implemented system but is an interesting topic for future work.

<p>Development of software-intensive systems such as embedded systems for telecommunications, avionics and automotives occurs under severe quality, schedule and budget constraints. As the size and complexity of software-intensive systems increase dramatically, the problems originating from the design and specification of the system architecture becomes increasingly significant. Architecture-based development approaches promise to improve the efficiency of software-intensive system development processes by reducing costs and time, while increasing quality. This paradox is partially explained by the fact that the system architecture abstracts away unnecessary details, so that developers can concentrate both on the system as a whole, and on its individual pieces, whether it's the components, the components' interfaces, or connections among components. The use of architecture description languages (ADLs) provides an important basis for verification since it describes how the system should behave, in a high level view and in a form where automated tests can be generated. Analysis and testing based on architecture specifications allow detection of problems and faults early in the development process, even before the implementation phase, thereby reducing a significant amount of costs and time. Furthermore, tests derived from the architecture specification can later be applied to the implementation to see the conformance of the implementation with respect to the specification. This thesis extends the knowledge base in the area of architecture-based verification. In this thesis report, an airplane control system is specified using the Architecture Analysis and Description Language (AADL). This specification will serve as a starting point of a system development process where developed architecture-based verification algorithms are applied.</p>

L'avantage majeur qu'offrent les services Web est le fait qu'ils reposent sur des standards et les technologies du Web pour interagir en s'échangeant des messages. A part les séquences de messages, d'autres facteurs affectent l'interopérabilité des services Web, telles que les contraintes temporelles qui spécifient les délais nécessaires pour échanger des messages. La thèse rapportée dans ce manuscrit étudie l'impact de ces propriétés dans la composition de services Web. La considération de telles propriétés soulève plusieurs problèmes auxquels on a essayé d'apporter une solution. Le premier aspect consiste à définir un modèle qui tienne compte des abstractions nécessaires afin de pouvoir analyser et synthétiser une composition, à savoir les messages, les données, les contraintes de données, les propriétés temporelles et l'aspect asynchrone des communications des services. En se basant sur ce modèle, le deuxième problème consiste à proposer une approche d'analyse de compatibilité. Cette analyse vise à caractériser la compatibilité ou la non-compatibilité des services Web et ce en prenant en considération les abstractions précédemment citées. Nous étudions particulièrement l'impact des propriétés temporelles dans une chorégraphie dans laquelle les services Web supportent des communications asynchrones. Nous proposons une démarche basée sur le model checking qui permet de détecter les éventuels conflits temporisés qui peuvent surgir dans une chorégraphie. Finalement, le dernier problème auquel nous nous intéressons est celui de la construction d'une composition qui essaie de répondre au besoin du client et ce en prenant en compte les aspects temporels. L'approche que l'on propose est basée sur la génération d'un médiateur pour essayer, quand c'est possible, de contourner les incompatibilités temporisées et non-temporisées qui peuvent surgir lors d'une collaboration. Des mécanismes et des algorithmes ont été développés afin de mettre en oeuvre ces objectifs.

The Virtual Network (VN) protocol is a communications protocol software compatible with the Space Plug-and-play Architecture (SPA). This Master Thesis defines a protocol that extends the Virtual Network protocol to cover communication over the Controller Area Network (CAN). The Virtual Network for the Controller Area Network (VN-CAN) is defined, modelled and verified using UPPAAL as well as implemented and tested while running on actual hardware. The VN-CAN protocol enables components on the CAN network to communicate with other components both inside and outside of the CAN network, which together with the modularity of both the protocol and the implementation enables application level software to be agnostic of their physical position in the network. The implementation enables components to automatically discover routes to other components on the VN network without the need for any prior knowledge about the network topology. A method for direct addressing, i.e. that two components on the CAN network can communicate directly without sending messages via a central router, has been added to the VN-CAN protocol in order to reduce traffic on the CAN network. UPPAAL modelling and verification of the VN-CAN protocol has been done to give a high level of confidence in the correctness of the protocol. Testing on actual hardware has shown that the protocol achieves the goals of address resolution, self addressing and transfer of VN messages over CAN.

In the context of Service-Oriented Systems (SOS), services represent loosely coupled discrete units that can be created, invoked, composed and decomposed upon a client request. In such a setting, where complex systems are composed out of services based on the client request, ensuring the expected level of Quality-of-Service (QoS) becomes a difficult task. In systems built on service-oriented principles, the formal specification of both functional and extra-functional system behavior, service availability, compatibility and interoperability between different services and systems have become important issues. To be compliant with the new features, the REMES language has been extended towards SOS with new constructs that have been given formal semantics. In this thesis, we propose transformation rules, definitions and techniques for transforming these new constructs into Timed Automata (TA) counterparts to facilitate the formal analysis. Also, we present an extension to an existing REMES SOS IDE toolset for performing an automated transformation of the REMES SOS models into the TA framework suitable for the formal analysis with the UPPAAL model-checker. The contribution from our work is on two fronts: a) define transformation rules for all of the constructs specific for the REMES SOS modeling and b) prototype implementation of the transformation rules as an extension add-on to the already existing IDE for modeling SOS to perform the automated transformation. The benefit of performing an automated transformation of the REMES SOS models in TA is twofold. First, by automating the transformation process, the process of validation of the models becomes faster. Second, we considerably reduce the influence from the human factor in the entire process, and at the same time lower the risks of introducing errors into the systems in the phase of creating the formal model. Additional benefit from the automated process is that the SOS designer does not have to be a verification expert in order to be able to verify the modeled system.

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.