Safety verification for ROS software

This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project PTDC/CCI-INF/29583/2017 (POCI-01-0145-FEDER-029583) and the PhD grant SFRH/BD/124836/2016. Safety Verification for ROS Applications André Filipe Faria dos Santos UMinho | 2021 Departamento de Informática André Filipe Faria dos Santos Safety Verification for ROS Applications Programa de Doutoramento em Informática das Universidades do Minho, de Aveiro e do Porto March 2021 Universidade do Minho Escola de Engenharia Departamento de Informática André Filipe Faria dos Santos Safety Verification for ROS Applications Tese de Doutoramento Programa de Doutoramento em Informática das Universidades do Minho, de Aveiro e do Porto Trabalho realizado sob a orientação do Professor Doutor Manuel Alcino Cunha e do Professor Doutor Nuno Moreira Macedo March 2021 DIREITOS DE AUTOR E CONDIÇÕES DE UTILIZAÇÃO DO TRABALHO POR TERCEIROS Este é um trabalho académico que pode ser utilizado por terceiros desde que respeitadas as regras e boas práticas internacionalmente aceites, no que concerne aos direitos de autor e direitos conexos. Assim, o presente trabalho pode ser utilizado nos termos previstos na licença abaixo indicada. Caso o utilizador necessite de permissão para poder fazer um uso do trabalho em condições não previstas no licenciamento indicado, deverá contactar o autor, através do RepositóriUM da Universidade do Minho. Licença concedida aos utilizadores deste trabalho Atribuição CC BY https://creativecommons.org/licenses/by/4.0/ ii ACKNOWLEDGEMENTS First, and foremost, I would like to express my deepest gratitude to my advisors, Professors Alcino Cunha and Nuno Macedo. They maintained a constant presence and guidance throughout the thesis, by reviewing my work, helping me stay on the right track, and pointing out routes and resources of relevance. Their expert knowledge was invaluable to formalise the approach this thesis proposes. Oftentimes our discussions were long and exhausting, but never fruitless. I have faced a fair share of obstacles and dead ends along the way. Without their support, however, I would have faced several more. I am also grateful to our colleagues from the Centre for Robotics in Industry and Intelligent Systems (CRIIS), from INESC TEC, namely Filipe Neves dos Santos, Luís Santos and Rafael Arrais. They are among the first adopters of our work and have provided us with one of our robot case studies. Seeing as it is still a system under development, without full documentation, I would have been lost in trying to understand it without their assistance. Besides, they have also contributed to the preliminary empirical study that we conducted at the very beginning of this thesis. I could not go by without extending my sincerest thanks to Mirko Bordignon, Nadia Hammoudeh García and a few other colleagues from Fraunhofer IPA. Our work has been widely promoted among the ROSIndustrial community, and I have participated in various relevant events, such as ROS-Industrial conferences and training sessions, all thanks to them. Furthermore, they are also among the early adopters of our work, and have been applying it to some of the robots built at Fraunhofer IPA, including the well-known Care-o-Bot. I also had the great pleasure of working with Andrzej Wasowski (IT University of Copenhagen), Gijs van der Hoorn (Delft University of Technology), Harsh Deshpande (Fraunhofer IPA) and Chris Timperley (Carnegie Mellon University), over the major part of this thesis, conducting empirical studies on common bugs that ROS developers face. We have had several enlightening discussions, and their feedback on my progress has been deeply appreciated. On a personal note, I must thank my parents and my partner Sofia for all the unconditional support they provided over these years. I thank them for a multitude of things, but especially for the small things of everyday life that one tends to take for granted, such as their patience. Many times they have listened to my rambling, even though they likely did not understand any of it. Lastly, I would like to acknowledge the financial support this work has received. This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project PTDC/CCI-INF/29583/2017 (POCI-01-0145-FEDER-029583) and the PhD grant SFRH/BD/124836/2016. iii STATEMENT OF INTEGRITY I hereby declare having conducted this academic work with integrity. I confirm that I have not used plagiarism or any form of undue use of information or falsification of results along the process leading to its elaboration. I further declare that I have fully acknowledged the Code of Ethical Conduct of the University of Minho. iv RESUMO Verificação de Propriedades de Correção em ROS Os robôs são agora parte do nosso quotidiano e a sua utilidade parece não ter limites. Fabricam os nossos bens, colhem alimentos de plantações e conduzem-nos de um lugar para o outro. A inovação na área da robótica é uma constante, as expectativas são altas, e as responsabilidades que depositamos nos robôs são cada vez maiores; os robôs são a nova definição de sistema crítico. Em parte, este sucesso deve-se à abundância de frameworks livres para o desenvolvimento de sistemas robóticos, como é o caso do Robot Operating System (ROS). A comunidade ROS é numerosa e bastante ativa. O ROS tem sido usado principalmente ao nível da investigação, mas, ultimamente, tem sido a base para vários projetos comerciais ou governamentais. Sendo um ecossistema de componentes de software reutilizáveis, suportado por uma comunidade muito diversa, garantir que sistemas baseados em ROS são confiáveis é da maior importância. No entanto, mostrar que um software robótico é confiável não é, de todo, uma tarefa fácil. Várias técnicas, como a Verificação Formal, Model Checking, Verificação Runtime, entre outras, têm dado inúmeras provas da sua aptidão e eficácia para verificar uma variedade de propriedades críticas, noutros domínios de software. Contudo, se há algo que todos estes métodos têm em comum, é a sua complexidade. É necessária uma formação especializada para uma aplicação eficaz, e a maioria da comunidade ROS não tem tais conhecimentos. Nesta tese, respondemos à questão de como adaptar o estado da arte em técnicas de garantia de qualidade para aplicações ROS, e como torná-las acessíveis a não especialistas. Temos em conta o facto de que a maioria dos sistemas são desenvolvidos em torno do código-fonte, em vez de seguirem práticas de Engenharia à base de modelos. Propomos um fluxo de trabalho unificado que, dado o código-fonte de uma aplicação ROS, extrai modelos automaticamente e, de seguida, aplica uma série de técnicas de verificação, estáticas e dinâmicas, relativamente a propriedades do sistema especificadas pelo utilizador. No caso de as análises detetarem uma violação de propriedades, os resultados podem ser utilizados como guias para a resolução de problemas. Caso contrário, os resultados constituem evidência da confiabilidade do sistema, respetivamente às propriedades, que pode ser usada para construção de um argumento de confiabilidade. Este fluxo de trabalho é implementado na plataforma HAROS, e avaliado com dois estudos de caso em robôs reais. O resultado revelou-se eficaz, quer na construção automática de modelos, quer na deteção de falhas, relativamente a propriedades especificadas pelo utilizador. De um modo geral, esta abordagem foi bem recebida pela comunidade ROS. Vários membros já a usam de forma independente, e estão até a propôr as suas próprias extensões. Palavras-chave: engenharia de software, métodos formais, robótica v ABSTRACT Safety Verification for ROS Applications Robots are now part of our daily lives and their usefulness is, seemingly, never-ending. They manufacture our goods, harvest our crops and drive us from place to place. Innovation in the field of robotics is constant, expectations are high, and the responsibilities we place on robots are ever increasing; robots are the new definition of safety-critical devices. In part, this success is due to the abundance of open source frameworks to help develop robotic systems, such as the Robot Operating System (ROS). ROS has a large and active community. It was mostly used in research, but is recently finding its way into commercial and government projects as well. With such a diverse community, and being based on an ecosystem of reusable software components, ensuring that ROS-based systems are dependable is paramount. However, showing that robotic software is dependable is not an easy task. Many techniques, such as Formal Verification, Model Checking, Runtime Verification, and more, have proved, over and over, to be capable of verifying a diverse range of properties in other software domains. However, if there is one characteristic that often defines these techniques, it is their steep learning curve. They have a hard requirement on expert knowledge, and the vast majority of the ROS community is composed of non-experts. In this thesis, we answer the research question of how to adapt state-of-the-art quality assurance techniques to ROS applications, and how to make them usable by non-experts. We take into consideration the fact that most systems are developed with a code-first approach, rather than following Model-driven Engineering practices. We propose a unified workflow that takes in ROS application code, automatically extracts system models from it, and then applies a variety of static and dynamic analysis techniques with respect to user-specified properties. If a property violation is detected, the results of the analyses can be used as a debugging aid. Otherwise, they provide compelling evidence to structure a dependability case for the given properties. This workflow is implemented in the HAROS framework, and later evaluated with two robot case studies. We have found this approach to be effective, both at building models and at finding faults for user-specified properties. Overall, it has been well-received in the ROS community. Several members are now independently using it, as well as proposing their own extensions. Keywords: lightweight formal methods, software engineering, robotics vi CONTENTS 1 Introduction 1 1.1 Context 2 1.1.1 On Building Robot Systems 2 1.1.2 The Robot Operating System 4 1.1.3 A Note on ROS2 5 1.2 Thesis Statement 5 1.3 Running Example: Fictibot 7 1.4 Contributions and Document Structure 8 2 The Robot Operating System 11 2.1 The Basics of ROS 11 2.1.1 Packaging and Distributing Software 11 2.1.2 Deployment and Runtime 14 2.2 Formal Methods and Quality Assurance for ROS 24 2.2.1 Model-based Techniques 24 2.2.2 Static Analysis Techniques 26 2.2.3 Dynamic Analysis Techniques 27 2.3 ROS in Practice 28 2.3.1 Corpus of the Study 29 2.3.2 RQ1 – Which ROS communication primitives are actually used, and how commonly? 31 2.3.3 RQ2 – In which context are these primitives used and how are their arguments defined? 33 2.3.4 RQ3 – What kind of features are typically used in ROS launch files to deploy applications? 35 2.3.5 RQ4 – How and how commonly is the ROS parameter server used? 37 2.3.6 RQ5 – How commonly are custom message and service types used in ROS communications? 37 2.3.7 Impact on Static Analysis 38 2.4 Summary 39 3 Modelling and Reverse-Engineering ROS Systems 40 3.1 State of the Art 40 3.1.1 Architectural Models 41 3.1.2 Model Extraction 42 3.2 A Metamodel for ROS Applications 46 3.2.1 Source Entities 48 vii list of figures xiv Figure 70 State machine monitoring for the Absence pattern. 174 Figure 71 State machine monitoring for the Existence pattern. 175 Figure 72 State machine monitoring for the Precedence pattern. 177 Figure 73 State machine monitoring for the Response pattern. 180 Figure 74 State machine monitoring for the Prevention pattern. 181 Figure 75 The TurtleBot2 robot. 194 Figure 76 The Random Walker Controller configuration. 195 Figure 77 The AMCL Navigation configuration. 195 Figure 78 The AgRob V16 agriculture robot monitoring a slope vineyard. 196 Figure 79 The AgRob V16 Basic and Path Planning configurations, the latter in dashed. 197 Figure 80 The evaluation system used in SemEval-2013. 201 Figure 81 The evaluation algorithm we use to assess the model extractor’s performance. 203 Figure 82 Example of a minimum weight matching. 204 Figure 83 Architecture of the MonPoly integration with a ROS system. 210 Figure 84 Hypothetical counterexample trace for the observed false negative. 222 Figure 85 Error report for the error found in the AgRob V16 Supervisor. 226 Figure 86 Counterexample trace for the first observed false negative. 228 Figure 87 Counterexample trace structure for the observed false negatives. 230 Figure 88 The fictibot_drivers package tree. 262 Figure 89 The fictibot_controller package tree. 269 Figure 90 The fictibot_multiplex package tree. 274 Figure 91 The fictibot_msgs package tree. 279 LIST OF TABLES Table 1 Corpus of packages used for the empirical study. 31 Table 2 Built-in parsing database for HAROS. 98 Table 3 Comparison of our custom monitor implementation versus MonPoly. 213 xv LIST OF LISTINGS 2.1 An example package manifest XML file. . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 An example CMake build file. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 Basic lifecycle of a C++ ROSnode............................ 16 2.4 Example of a custom ROS msg with a field and a constant. . . . . . . . . . . . . . . . 17 2.5 A minimal node with a publisher and a subscriber. . . . . . . . . . . . . . . . . . . . 18 2.6 A minimal node using a service server. . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 A minimal node using a service client. . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.8 A minimal node reading and writing parameters. . . . . . . . . . . . . . . . . . . . . 20 2.9 TheROStimeprimitives. ............................... 22 2.10 A minimal launch file for Fictibot. . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.11 A minimal launch file for Kobuki. . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1 Specifying subscriber information as launch file comments [170]. ........... 46 3.2 YAML specification of a Source File. . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.3 YAML specification of a Package. . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.4 YAML specification of a Repository. . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.5 YAML specification of a Project. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.6 YAML specification of a Node (excerpt). . . . . . . . . . . . . . . . . . . . . . . . . 52 3.7 YAML specification of a Node Instance (excerpt). . . . . . . . . . . . . . . . . . . . . 54 3.8 YAML specification of a Configuration (excerpt). . . . . . . . . . . . . . . . . . . . . 57 3.9 Overview of the model extraction algorithm. . . . . . . . . . . . . . . . . . . . . . . 58 3.10 The fictibot_controller node, identified in the CMakeLists.txt file........... 59 3.11 The main function of the src/controller_node.cpp file................. 60 3.12 Overview of the configuration construction algorithm. . . . . . . . . . . . . . . . . . . 61 3.13 The fictibot_controller launch/multiplexer.launch file. ............. 62 3.14 Some of the topics used in the src/random_controller.cpp file of fictibot_controller . 62 3.15 Example extraction hints in YAML syntax. . . . . . . . . . . . . . . . . . . . . . . . 64 5.1 Minimal project file for Fictibot. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 5.2 Interface through which plug-ins communicate with HAROS. . . . . . . . . . . . . . . 91 5.3 Excerpt of a JSON data file exported by HAROS. . . . . . . . . . . . . . . . . . . . . 92 5.4 Plug-in manifest file in YAML syntax. . . . . . . . . . . . . . . . . . . . . . . . . . . 94 5.5 Excerpt of the HAROS plug-in for the Radon Python tool. . . . . . . . . . . . . . . . . 95 5.6 Minimal project file for Fictibot with configurations. . . . . . . . . . . . . . . . . . . . 97 5.7 Project file for Fictibot with a configuration and extraction hints. . . . . . . . . . . . . 97 xvi list of listings xvii 5.8 Project file for Fictibot with plug-in-specific input data. . . . . . . . . . . . . . . . . . 98 5.9 Basic query to identify topics with multiple publishers. . . . . . . . . . . . . . . . . . 103 5.10 Basic query to identify topics with multiple publishers. . . . . . . . . . . . . . . . . . 103 5.11 Plug-in manifest file for the Pyflwor plug-in. . . . . . . . . . . . . . . . . . . . . . . 104 5.12 Project file for Fictibot with a configuration and Pyflwor queries. . . . . . . . . . . . . 104 5.13 Entry point function of the Pyflwor plug-in. . . . . . . . . . . . . . . . . . . . . . . . 105 5.14 Query catalogue to run over Fictibot’s Computation Graph. . . . . . . . . . . . . . . . 107 7.1 Trivial example of using Hypothesis. . . . . . . . . . . . . . . . . . . . . . . . . . . 170 7.2 Using Hypothesis strategies to build ROS messages. . . . . . . . . . . . . . . . . . . 171 7.3 Top-level function to generate test scripts from annotated Configurations. . . . . . . . . 185 7.4 Function to identify open subscribed topics in a Configuration. . . . . . . . . . . . . . 186 7.5 Function to build test scripts using schemas and code templates. . . . . . . . . . . . 186 7.6 Hypothesis strategy for 8-bit signed integers. . . . . . . . . . . . . . . . . . . . . . . 187 7.7 Strategy for geometry_msgs/Twist messages......................188 7.8 Strategy for std_msgs/Int8 messages such that data ≤50...............189 7.9 Example strategy to generate message traces. . . . . . . . . . . . . . . . . . . . . . 190 7.10 Main Hypothesis test function. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191 8.1 Excerpt of a ground truth model, illustrating a node with a publisher. . . . . . . . . . . 202 A.1 The package.xml file..................................262 A.2 The CMakeLists.txt file.................................263 A.3 The include/fictibot_drivers/motor_manager.h file. ..................264 A.4 The include/fictibot_drivers/sensor_manager.h file...................265 A.5 The src/motor_manager.cpp file(part1of2)......................266 A.6 The src/motor_manager.cpp file(part2of2)......................267 A.7 The src/sensor_manager.cpp file............................268 A.8 The src/driver_node.cpp file. .............................269 A.9 The package.xml file..................................270 A.10 The CMakeLists.txt file.................................270 A.11 The include/fictibot_controller/random_controller.h file.................271 A.12 The src/random_controller.cpp file(part1of2).....................272 A.13 The src/random_controller.cpp file(part2of2).....................273 A.14 The src/controller_node.cpp file. ...........................274 A.15 The launch/minimal.launch file.............................274 A.16 The launch/multiplexer.launch file. ..........................274 A.17 The package.xml file..................................275 A.18 The CMakeLists.txt file.................................275 A.19 The include/fictibot_multiplex/trichannel_multiplex.hpp file...............276 A.20 The src/trichannel_multiplex.cpp file(part1of3)....................277 A.21 The src/trichannel_multiplex.cpp file(part2of3)....................278 list of listings xviii A.22 The src/trichannel_multiplex.cpp file(part3of3)....................279 A.23 The src/multiplex_node.cpp file. ...........................279 A.24 The package.xml file..................................280 A.25 The CMakeLists.txt file.................................280 A.26 The msg/Custom.msg file. ..............................280 C.1 The plugin.yaml file. .................................302 C.2 The plugin.py file(part1)................................303 C.3 The plugin.py file(part2)................................304 C.4 The pyflwor_monkey_patch.py file. ..........................305 C.5 Project file for Fictibot with Pyflwor queries (part 1). . . . . . . . . . . . . . . . . . . 306 C.6 Project file for Fictibot with Pyflwor queries (part 2). . . . . . . . . . . . . . . . . . . 307 1 INTRODUCTION Mankind has always dreamt of machines capable of remarkable feats of intelligence and human-like behaviour. Robots are only a few decades old, but they are the culmination of more than two thousand years of technical evolution [76]. With the advent of the Third Industrial Revolution, in the 1960s, we transitioned from analog, mechanical and electronic technology to the digital technology we know and use. Coincidentally, this transition, that marks the dawn of the Information Age [ 137 , 144 ], also characterises the recent advances in robotics. The common factor that enables this rapid progress is none other than software. The benefits of software over the traditional technologies is evident, and it did not take long until software became ubiquitous. It proliferated and took control of the emerging technologies, such as digital computers, cell phones, the Internet and, recently, robots. Robots are now part of our daily lives and their usefulness is, seemingly, never-ending. They manufacture our goods, harvest our crops and drive us from place to place. They are the cornerstone of the Fourth Industrial Revolution, also known as Industry 4.0, and their numbers are ever-increasing. It is estimated that the worldwide operational stock of industrial robots has reached more than 3 million units in the year of 2020 [82], and will reach almost 4 million by 2022. Robots are now performing feats that could only take place in science fiction, a few decades ago. For instance, the city of Seoul, in South Korea, has planned the construction of the Robot Science Museum starting in the year of 2020, expected to finish in the year of 2022. What is unique about this museum is that its first exhibition will start even before it opens – the façade of this museum will be entirely built by construction robots and drones [ 30 ]. Besides being a unique feat in the history of robotics, the intent behind this project is to support public education in robotics and raise awareness of artificial intelligence initiatives. Robots have also proved their usefulness under exceptional circumstances. In 2020, the COVID-19 global pandemic has completely changed everyday life – remote work and social distancing became new realities, and hygiene is more imperative than it ever was. During these uncertain times, in which public health is a top priority and the global economy has taken a major hit, robots come to the rescue. Hospitals have employed mobile robots to deliver sterile goods and ensure that they do not run out of stock [ 87 ]; certain public spaces are sanitised using mobile robots mounted with ultraviolet light attachments [ 88 ]; cafes replace human waiters with robotic waiters; and the list goes on. As many jobs and workplaces become extremely conditioned, the economy relies more on robotics to recover. 1 1.1. Context 2 There is no doubt that robots are capable of incredible things. Innovation is constant, expectations are high, and the responsibilities we place on robots are ever increasing. Robots are the new definition of safety-critical devices. But, what can we say about their overall software quality? In this thesis, we will explore how can some aspects of software quality be improved in robotic systems. 1.1 Context 1.1.1 On Building Robot Systems Primitive robot systems, much like any relatively new technology, were built mostly in an ad hoc fashion. Over time, some software architectures thrived and became standards among practitioners. One of the first major archetypes, that gained popularity in the first half of the decade of 1980, was the Sense-Plan-Act architecture (SPA) [ 130 ]. It was believed in the Artificial Intelligence community that a robotic system should be decomposed into three functional elements, as shown in Figure 1: a sensing system, a planning system and an execution system. The sensing system was responsible for translating raw sensor data into a world model. The planning system took the world model and a mission goal, such as moving towards a given location, and generated a plan to achieve the given goal. The execution system translated the action plan into concrete actions and commands that could be issued to the robot’s actuators. This type of architecture is generally known as deliberative . Figure 1: The Sense-Plan-Act robot architecture. The SPA architecture is an open loop architecture; control flows in one direction, and feedback is never taken into consideration. As a consequence, this architecture does not handle environmental uncertainty and unpredictability very well. The intelligence of this approach, such as it is, resides in the plan generator, which is generally slow and dependent on an accurate model of the world. It turned out that world modelling and plan generation were later classified as Very Hard Problems. It did not take long for alternative architectures to be proposed. In the mid 1980s, Rodney Brooks proposed the Subsumption architecture [ 33 ], the most common departure from the previous paradigm. The Subsumption architecture, as seen in Figure 2, is a reactive , behaviour-based architecture; it lives on the opposite end of the spectrum, relative to the SPA architecture. 1.1. Context 3 Figure 2: The Subsumption robot architecture. Subsumption set aside the problems of modelling and planning, to emphasise the coupling of the robot’s immediate sensing and actions. The robot’s behaviours were decomposed in several layers, representing progressively more complex tasks. Each layer was, essentially, a state machine that handled raw sensor data directly. Layers were composed together, and relied on a process called suppression or inhibition, that ensured that higher-priority behaviours would override less critical ones. Its basis on very simple, stateless and low-level computations had a dramatic effect on performance. Collision-free mobile robots, for instance, were much more performant when built on top of a reactive architecture. On the other hand, it appeared to have a capability ceiling, as it had no means to manage very complex behaviours; it was not sufficiently modular. In the early 1990s, researchers agreed that none of the two extremes would be the right answer for every problem. Their views converged, and hybrid architectures became the new norm. In particular, the Three-Layered architecture [ 75 ] (Figure 3) was one of the most prominent. This architecture is comprised of three elements: • a reactive Controller, that tightly couples sensors and actuators, and operates with fast, stateless algorithms to implement primitive behaviours; • a Sequencer, or plan executer, that selects the most appropriate behaviour at any given time, and supplies the necessary parameters; • a Deliberator, that handles planning, world models, internal state representation, and all timeconsuming computations in general. Figure 3: The Three-Layered robot architecture. 1.1. Context 4 As we can see in Figure 3, the Three-Layered architecture organises its components by time and space complexity. The different layers cooperate, rather than inhibit each other. As robots become more ubiquitous and the hardware becomes cheaper and more capable, the demands we place on robotic systems increase without an end on sight. The size and complexity of robotics software got out of hand for the existing architectures. New concepts and paradigms from other software domains were adopted, such as publisher-subscriber communications in distributed systems, and, eventually, standardised in a number of middlewares. Among the most common middlewares are YARP 1 , Orocos 2 , Player 3 and the Robot Operating System 4 . The last is now a de facto standard [ 45 , 61 , 73 , 115 ], and is the application domain of this thesis. 1.1.2 The Robot Operating System The Robot Operating System [ 143 ] (ROS) started in 2007 as a collaborative effort, led by Willow Garage 5 , to provide the robotics community a common, free, open-ended development platform. This initiative, which in its first few iterations was essentially a communication middleware, quickly evolved, adding numerous tools, drivers, software components and libraries to its arsenal. It did not take long for ROS to match and supersede its competitors, e.g., the Player project, in terms of suitability for the task, easier learning curve, support and documentation. Now, nearing three thousand software packages in the official distribution, ROS is the de facto standard in robotics research, paving its way into commercial and government applications, backed by a large and active community. Indeed, the community is one of the strongest aspects of ROS. Notably, some of the main developers and researchers behind ROS established the Open Source Robotics Foundation 6 , a non-profit organization (the first of its kind) dedicated to sustaining and improving open source robotics software, such as ROS itself and the Gazebo 7 robot simulator. Other initiatives, such as ROS-Industrial 8 , ROS-Military 9 or ROS-Agriculture 10 empower and drive the adoption of ROS in specific commercial domains. More recently, a number of other, smaller groups within the community is also emerging. Among these, the ROS Quality Assurance Working Group 11 , a group focused on improving Quality Assurance in the ROS ecosystem, is the most relevant to our work. Since 2012, there is a yearly conference, ROSCon 12 , where hundreds of developers of all levels (over 500 in the 2018 edition) have a chance to meet and share projects, ideas and research results centered on ROS. The ROS-Industrial initiative also has its own yearly conference since 2013, although with a smaller audience and a focus on industrial applications and software best practices. Parallel to 1http://www.yarp.it/index.html 2https://orocos.org/ 3http://playerstage.sourceforge.net/ 4https://www.ros.org/ 5http://willowgarage.org/ 6http://osrfoundation.org/ 7http://gazebosim.org/ 8https://rosindustrial.org/ 9https://rosmilitary.org/ 10 http://rosagriculture.org/ 11 https://discourse.ros.org/c/quality 12 https://roscon.ros.org 1.2. Thesis Statement 5 these, developers worldwide organize regular regional meetups as well. Last, but not least, the community has worked on a few invaluable online resources, such as: • the ROS Wiki13, where over 8 000 users share 117 000 pages of documentation and tutorials; • ROS Answers 14 , a website with more than 34 000 users where community members ask and answer ROS-related questions; • ROS Discourse 15 , a forum with more than 4 000 users, where the community discusses projects, ROS-Industrial, Quality Assurance, embedded systems, and more. 1.1.3 A Note on ROS2 Traditionally, ROS has followed a release cycle that is similar to Unix distributions, as we will see in Chapter 2. Newer versions introduced changes that, in many cases, did not break existing code. However, the field of robotics is in constant evolution, and its needs change as well. ROS grew way beyond its initial vision, and so, in December 2017, the development team released ROS2, a new major version, that is mostly incompatible with the former. It relies on state-of-the-art technologies, and aims to cover new use cases that ROS did poorly, or not at all. For instance, ROS2 has been designed from the start to be suitable for: • teams of multiple robots (which is possible in ROS, but there is no standard approach); • small embedded platforms, such as micro controllers; • real-time systems, provided operating system support; • networks with poor connectivity; • production environments (again, possible with ROS, but not ideal). The long term plan is for ROS2 to eventually replace ROS. Currently, both versions of ROS exist in parallel, and development for the original version is set to continue, at least, until 2025. Many users (especially companies) are slowly migrating towards the new version, but there are many systems already in place that work only with the original ROS. Since the original version is stable, and was the only released version when this thesis project began, our research will focus solely on ROS, not on ROS2. 1.2 Thesis Statement It is undeniable that ROS is finding its way into various safety-critical applications. Despite being rooted in relatively harmless research robots, ROS is now the backbone of industrial robots, agriculture robots and more. Safety cages are no more; expensive, powerful robots move freely in unstructured environments, interacting closely with humans, animals, plants and precious goods. We want to be sure that our robots 13 http://wiki.ros.org/ 14 https://answers.ros.org 15 https://discourse.ros.org 2.1. The Basics of ROS 12 In a ROS environment, software is organised in packages , the basic build and release units. Over time, distributions became very large, surpassing 4000 packages in ROS Melodic Morenia. Furthermore, there are many open-source packages that are not part of the official distributions. It does not come as a surprise that most users need only a relatively small number of these packages. To accomodate for this scenario, distributions typically offer installations in four different levels, as seen in Figure 6. Figure 6: Package organisation within a ROS distribution. •ROS Base is the bare bones installation; it offers the core functionality and command line tools for users to build their own ROS packages and applications. •ROS Desktop offers the Base features, plus a few graphical tools and robot-generic libraries. •ROS Desktop-Full offers ROS Desktop packages, plus navigation and perceptions libraries, as well as 2D and 3D simulators. •ROS Distribution offers a vast range of officially indexed packages that include all of the above and more; cannot be installed directly via convenient commands as the previous levels. In addition, individual packages, not included in the groups above, can always be hand-picked and installed at any time. A package has only three hard requirements, as follows. Figure 7shows the structure of a minimal package. 1. A package must have its own directory; nested packages or multiple packages in a single directory are not allowed. 2. A package must contain a manifest file – an XML file, called package.xml , with meta information about the package. 3. A package must contain a CMake build file ( CMakeLists.txt ), using the appropriate macros for the ROS build system. Besides the CMake and package XML files, a package can contain nearly anything, from source code to robot models, from configuration files to standalone tools. 2.1. The Basics of ROS 13 Figure 7: Example of a minimal ROS package. The package manifest defines basic properties about a package, such as the package’s name, version number, authors, maintainers, licenses, and dependencies on other ROS packages. Listing 2.1 illustrates the package.xml file of a controller component, for our Fictibot robot, the running example we use throughout the thesis. In this file, we can see the <name> tag defining the fictibot_controller name for the package, the <version> tag defining the version number 0.1.0 and the <description> tag providing a free text description. We can also see author and maintainer information in the <author> and <maintainer> tags, respectively, along with an MIT license in the <license> tag. Finally, we define some dependencies, such as catkin – the standard package building tool for ROS – in the <buildtool_depend> tag, as well as the roscpp,std_msgs and fictibot_msgs ROS packages, in the <depend> tag. 1<?xml version="1.0"?> 2<package format="2"> 3<name>fictibot_controller</name> 4<version>0.1.0</version> 5<description>The fictibot_controller package.</description> 6<author email="[email protected]">André Santos</author> 7<maintainer email="[email protected]">André Santos</maintainer> 8<license>MIT</license> 9<buildtool_depend>catkin</buildtool_depend> 10 <depend>roscpp</depend> 11 <depend>std_msgs</depend> 12 <depend>fictibot_msgs</depend> 13 </package> Listing 2.1: An example package manifest XML file. The catkin build system uses CMake, thus the need for a CMakeLists.txt file. There are a few requirements regarding the contents of this file, such as declaring dependencies on other packages, which end up duplicating information between CMakeLists.txt and package.xml . We will not delve into detail for all available functions and macros, as such information is not relevant for this work. Listing 2.2 shows an example CMake file for the same Fictibot controller package. In this example, we can see the name of the package, declared in project , package dependencies after CATKIN_DEPENDS , directories where C ++ header files can be located, in include_directories , as well as which executables are built from this package, in add_executable,add_dependencies and target_link_libraries. Sometimes, packages are closely related, and meant to be used in conjunction. For instance, in Fictibot, it would make sense to install both a package for the robot drivers as well as for a high-level controller, since the driver, by itself, does not do much. This is a common pattern in many robots, such as TurtleBot2 2 or 2https://www.turtlebot.com/turtlebot2/ 2.1. The Basics of ROS 14 1cmake_minimum_required(VERSION 2.8.3) 2project(fictibot_controller) 3find_package(catkin REQUIRED COMPONENTS roscpp std_msgs fictibot_msgs) 4catkin_package( 5INCLUDE_DIRS include 6CATKIN_DEPENDS roscpp std_msgs fictibot_msgs 7) 8include_directories(include ${catkin_INCLUDE_DIRS}) 9add_executable(fictibot_controller 10 src/controller_node.cpp src/random_controller.cpp) 11 add_dependencies(fictibot_controller 12 ${${PROJECT_NAME}_EXPORTED_TARGETS} ${catkin_EXPORTED_TARGETS}) 13 target_link_libraries(fictibot_controller ${catkin_LIBRARIES}) Listing 2.2: An example CMake build file. the Care-O-bot 4 3 . Another example is for libraries that provide similar functionality, such as navigation algorithms. In these cases, it is possible to group packages together with a metapackage . A metapackage is simply a package with no contents (besides the mandatory files) that declares runtime dependencies on the packages that it is meant to group together. Thus, when a metapackage is installed, all of its dependencies should also be installed. It is a clever mechanism to circumvent the restrictions on nested packages. 2.1.2 Deployment and Runtime The ROS Computation Graph A typical ROS system is a distributed system, with various independent resources connecting to each other through various means. This network of resources is called the ROS Computation Graph . Every resource in the graph is named, with a hierarchical naming structure. For instance, both the names /max_vel and /robot/max_vel represent resources named max_vel , but the former is said to be under the global namespace , while the latter is under a /robot namespace . In this case, the first example might represent a maximum velocity parameter for all components in the system, while the latter could represent the maximum velocity of an individual robot in the network. The intent of using namespaces is to provide encapsulation. In general, a resource can create other resources within its namespace, and it can access resources within or above its namespace. I.e., /robot can access /max_vel and /robot/max_vel , but it can only create /robot/max_vel . In practice, this is just a convention, and any resource can access any other resource using its full name. A full ROS name is a series of identifiers separated (and preceded) by forward slashes, as in the previous examples. However, ROS provides a name resolving mechanism to avoid specifying full names all the time. As such, a name is said to be: 1. a base name if it is a simple identifier, e.g., max_vel; 3https://www.care-o-bot.de/en/care-o-bot-4.html 2.1. The Basics of ROS 15 2. relative if it is a series of identifiers separated by forward slashes, e.g., robot/max_vel; 3. private if it starts with a tilde, e.g., ~max_vel; 4. global if it is a full name, starting with a forward slash, e.g., /robot/max_vel. From the definitions above, we can see that base names are also relative names. Private names are a shortcut notation to resolve a name relative to the querying resource’s own namespace. For instance, if /robot wants to access ~max_vel , ROS will look for /robot/max_vel . Relative names are resolved relative to the namespace the querying resource is in. For instance, if /robot wants to access max_vel , ROS will look for /max_vel , and not /robot/max_vel , because /robot lives in the global namespace, i.e., / . Global names are considered to be fully resolved. As a final note on names, at runtime initialisation, any name can be remapped into any other name. This works as an intermediary look up table for each resource. It is a transparent mechanism to redirect names, without changing source code. For example, suppose there are two resources named /robot1 and /robot2 . If a remapping from /max_vel to /max_vel1 is defined for /robot1 , whenever /robot1 tries to access /max_vel , it will be transparently accessing /max_vel1 instead. /robot2 works normally, as remappings are not global. Naturally, remappings play a big role when composing software from different packages into a single system, since source code does not have to be changed for resources to be able to access each other. ROS Graph Resources Up to this point, resources were presented in abstract terms. Now, we shall go over the four main types of resources in a ROS system: nodes , topics , services and parameters . Nodes are the main resources in a Computation Graph. They are processes that consume, process and produce data. They communicate with each other via message-passing. The other types of resources either hold shared data (parameters) or serve as message-passing channels (topics and services). One of the main design principles of ROS is that nodes should be specific and modular, rather than monolithic components. It is normal for a single robot to have a network of many nodes. For instance, in the Fictibot example there is the /fictibase node that runs the robot’s drivers, providing access to sensors and actuators, and the /ficticontrol node that provides a high-level controller. In a more realistic example, there might be nodes for localisation, navigation or perception, and each sensor and actuator might have its own individual node. Nodes are written using one of the ROS client libraries, such as roscpp (for C ++ ) and rospy (for Python), and they typically follow a common lifecycle, shown in Listing 2.3, although this is not mandatory. 2.1. The Basics of ROS 16 1#include <ros/ros.h> 2 3void main_loop() { 4// Option 1 5ros::spin(); // loop until shutdown is requested; 6// process incoming messages as they arrive 7// Option 2 8ros::Rate loop_rate(10); // aim for a 10 Hz loop 9while (ros::ok()) { // repeat until shutdown is requested 10 ;// read sensors, create messages, update maps, etc. 11 ros::spinOnce(); // process all pending received messages 12 loop_rate.sleep(); // sleep the remaining time to meet the 10 Hz rate 13 } 14 } 15 16 int main(int argc, char **argv) { 17 ros::init(argc, argv, "node_name"); // register as a ROS node 18 // read and write parameters 19 // create topics and services 20 main_loop(); 21 return 0; 22 } Listing 2.3: Basic lifecycle of a C++ ROS node. In Listing 2.3 we can see the use of the ros::init function, which registers the process as a ROS node in the Computation Graph, using the name given as its third argument. Before any real work is done, there is usually a setup phase, during which the node reads and writes ROS parameters that it might need, as well as creating (or connecting to) a series of message-passing channels (topics or services). Once this ROS interface is all set up, the node enters its main loop, which should run until a user requests the shutdown of the ROS system. There are two main options for this loop, as shown in the example. The first is simply a call to the ros::spin() function, which blocks the process indefinitely, simply waiting for new messages. Once a message arrives, it should automatically trigger the respective reaction function, as we will explain. The second option is to put together the loop manually, using while (ros::ok()) to detect the user’s request to shut down. Within this loop, the user is free to perform any actions. The most common actions are a call to ros::spinOnce() , which processes any incoming messages that might be pending at the moment, and some sort of waiting mechanism, a variant of sleep() (which we also explain later), so that iterations occur at a certain rate, rather than continuously. There is a node variant, called nodelet , that is designed to bolster the performance of tightly coupled nodes, i.e., nodes that are meant to share many (possibly large) messages and are closely related to each other (e.g., image processing nodes). A nodelet runs on a single thread, rather than a process, and multiple nodelets can be grouped under a nodelet manager that spawns the main process. The main advantage of nodelets is that ROS is able to transparently share messages between nodelets via shared memory, rather than sending messages over the network. A limitation of nodelets is that, being threads of a process, they must reside on the same machine. Nodelets are able to communicate with regular nodes, using the standard mechanisms. 2.1. The Basics of ROS 17 In every ROS system there is a special node, not implemented by the user, called the ROS Master , that provides the naming service for the whole Computation Graph. Nodes communicate with the Master to register themselves with a given ROS name, e.g., /fictibase , and to discover other nodes in the network, e.g., /ficticontrol . Nodes must also communicate with the Master to create and access resources in the Computation Graph, such as topics, services and parameters. For instance, when a node is interested in accessing a certain topic, the Master shares with it the list of other nodes that are also accessing the same topic name. This is all done transparently to the user, using certain functions of the ROS client libraries, as we will see in the remainder of this section. As to how nodes actually send messages to each other, by default, there is a choice between the aforementioned topics and services. Both are typed, meaning that when a resource is created, a message type is registered along with the name, and all nodes are expected to send and receive messages of that type only. Type checking is done only at runtime, by comparing MD5 checksums for the message type. The ROS Base set of packages provides a number of standard message types (e.g., primitive data types, laser scans, 3D poses, etc.), but users can also define their own custom messages. Message types are defined in .msg files for topic messages and in .srv files for services, using a domain-specific language. The package building system provides the tools to automatically generate source code for the different client libraries. Listing 2.4 shows an example of a custom .msg file declaring a constant, THE_NUMBER , and two message fields, a_number and stamp . When messages are sent, only the fields are actually serialised and transmitted. Constants are defined for convenience, e.g., to check that a_number == THE_NUMBER . Field types can be primitive types, time stamps, durations or other message types, to allow the definition of complex messages via composition. Fields can also be fixed-length arrays or variable-length lists of any of the previous types. 1# Lines starting with `#' are comments. 2# Constants are defined with the `=' sign. 3uint8 THE_NUMBER = 42 4# Fields only declare a type and a name. 5time stamp 6uint8 a_number Listing 2.4: Example of a custom ROS msg with a field and a constant. Topics are the most common message-passing mechanism, as we will see in Section 2.3. They follow an asynchronous publisher-subscriber model, with many to many connections. Publishers can send messages at any time, regardless of the number of active subscribers, and subscribers are notified (via a callback function), once a new message is received. Both publishers and subscribers are backed by a message queue whose size is defined by the user. Messages are processed in order. If a message queue is full and a new message arrives, the oldest message is discarded silently. Before a node is able to publish any messages on a topic it must advertise said topic. In practice, this is the step where the node registers itself on the Master as a publisher, and gets back the current list of subscribers. This type of communication is ideal for continuous data streams, such as sensor data. Listing 2.5 is an adaptation of 2.1. The Basics of ROS 18 the publisher-subscriber tutorial from the official ROS Wiki 4 , and shows a minimal example of publishing to a topic out and subscribing to a topic in . The latter receives messages of the standard type std_msgs/UInt8 (8-bit unsigned integer), while for the former we use the custom message type defined in Listing 2.4, assuming it is called tutorials/Custom. 1#include <ros/ros.h> 2#include <std_msgs/UInt8.h> 3#include "tutorials/Custom.h" 4 5void callback(const std_msgs::UInt8::ConstPtr& msg) { 6// do something with `msg'... 7} 8 9int main(int argc, char **argv) { 10 ros::init(argc, argv, "node_name"); // register as a ROS node 11 ros::NodeHandle n; 12 13 ros::Publisher pub = n.advertise<tutorials::Custom>("out",10); 14 ros::Subscriber sub = n.subscribe("in",10, callback); 15 16 ros::Rate loop_rate(10); // aim for a 10 Hz loop 17 while (ros::ok()) { // repeat until shutdown is requested 18 tutorials::Custom msg; 19 msg.stamp = ros::Time::now(); 20 msg.a_number = Custom::THE_NUMBER; 21 pub.publish(msg); // `msg' is sent at this point 22 23 ros::spinOnce(); // process incoming messages with `callback' 24 loop_rate.sleep(); // sleep the remaining time to meet the 10 Hz rate 25 } 26 return 0; 27 } Listing 2.5: A minimal node with a publisher and a subscriber. We can see in lines 13 and 14 the creation of a Publisher channel and a Subscriber channel, respectively. Both use the creation functions with the least possible parameters. For the Publisher , in C ++ , we have to instantiate the template function advertise on the spot, by providing the desired message type (in this case, tutorials::Custom ). The first parameter, given the argument "out" , defines the desired ROS name for the topic (which is subject to name remappings), while the second parameter defines the desired message queue size. The call to subscribe is similar, except that the message type is given from its third parameter – a pointer to a callback function that processes incoming messages. Services are the second message passing method provided by the core ROS interface. This method implements synchronous one to one communication, using remote procedure calls. So, in this case, there is a notion of server (the node that provides the service) and client (the node that uses the service). It is considered an error to have multiple servers for a service with the same name. Messages are exchanged in request-response pairs, and clients block while waiting for a response. Ideally, services are used for quick tasks, such as querying the current state of a node. Long tasks should avoid using services because 4http://wiki.ros.org/ROS/Tutorials/WritingPublisherSubscriber%28c%2B%2B%29 2.1. The Basics of ROS 19 it might lead to unresponsiveness, as other messages queue up. Similar to publishers, a service server must also advertise the service to the ROS Master before clients can request it. Listings 2.6 and 2.7 are an adaptation of the service tutorial 5 , and show minimal nodes advertising and requesting a service that adds two integers, respectively. 1#include <ros/ros.h> 2#include "beginner_tutorials/AddTwoInts.h" 3 4bool add(beginner_tutorials::AddTwoInts::Request &req, 5beginner_tutorials::AddTwoInts::Response &res) { 6// request `req' contains two integers `a' and `b' 7// response `res' contains a field `sum' to hold the result 8res.sum = req.a + req.b; 9return true; 10 } 11 12 int main(int argc, char **argv) { 13 ros::init(argc, argv, "add_two_ints_server"); // register as a ROS node 14 ros::NodeHandle n; 15 16 ros::ServiceServer server = n.advertiseService("add_two_ints", add); 17 18 ros::spin(); // loop, processing messages, until shutdown is requested 19 return 0; 20 } Listing 2.6: A minimal node using a service server. 1#include <ros/ros.h> 2#include "beginner_tutorials/AddTwoInts.h" 3 4int main(int argc, char **argv) { 5ros::init(argc, argv, "add_two_ints_client"); // register as a ROS node 6ros::NodeHandle n; 7 8ros::ServiceClient client = 9n.serviceClient<beginner_tutorials::AddTwoInts>("add_two_ints"); 10 11 beginner_tutorials::AddTwoInts srv; 12 srv.request.a = 12; 13 srv.request.b = 15; 14 15 if (client.call(srv)) { 16 ROS_INFO("Sum: %ld", (long int) srv.response.sum); 17 }else { 18 ROS_ERROR("Failed to call service add_two_ints"); 19 return 1; 20 } 21 return 0; 22 } Listing 2.7: A minimal node using a service client. 5http://wiki.ros.org/ROS/Tutorials/WritingServiceClient%28c%2B%2B%29 2.1. The Basics of ROS 20 There is a third communication mechanism worth mentioning, called actions . Actions are not provided by the core ROS interface, but rather by the actionlib library, that has been part of the official distributions since ROS Indigo Igloo. They use several topics under the hood, but are similar to services, in the sense that there is a client-server model. The main difference is that actions are intended to fill the gap left by services for long-running tasks on demand. In this case, request and response (called goal and result, respectively) are asynchronous, i.e., the client sends a goal, and does not block while waiting for a result. Rather, the client is notified, via callback functions, of the progress towards the goal, and, later, of the result itself. The main advantage of actions is that, at any time, the client has the option to preempt the computation. Also, at any point, the client is able to block waiting for a result, just as if using services. Good examples of actions are moving a robot to a certain location, or identifying an object from visual feedback (perception). Seeing as they are not a core communication mechanism, but, rather, an abstraction built on top of the other primitives, this thesis will be focusing only on topics and services. The final type of resource, parameters, is used to share data with (or between) nodes, but without messages, or any kind of explicit communication for that matter. The ROS Master holds a shared key-value store, called the Parameter Server , where keys are ROS names and values can be any primitive type, ISO 8601 dates, base64-encoded binary data or lists of such values. Any node (or user, e.g., via a command line) can read and write values on the server. The Parameter Server is not designed for high-performance access; its main purpose is to hold static configuration parameters. For instance, if a node needs to read a file at runtime, instead of hard-coding the filename in the source code, a path can be fetched from a string parameter. Users would set the appropriate parameter before starting the node, resulting in a much more modular solution. Listing 2.8 illustrates this example. 1#include <string> 2#include <iostream> 3#include <fstream> 4#include <ros/ros.h> 5 6int main(int argc, char** argv) { 7ros::init(argc, argv, "file_writer"); 8ros::NodeHandle n; 9std::string file_path; // storage for parameter value 10 if (n.getParam("~file_path", file_path)) { // getParam reads the parameter 11 std::ofstream input_file(file_path); // open file for writing 12 if (input_file.is_open()) { 13 input_file << "This file was given via ROS parameters.\n"; 14 input_file.close(); 15 n.setParam("~succeeded",true); // write true on the parameter 16 } 17 }else { 18 n.setParam("~succeeded",false); // write false on the parameter 19 } 20 return 0; 21 } Listing 2.8: A minimal node reading and writing parameters. 2.1. The Basics of ROS 21 When reading and writing parameters, namespaces have a special meaning. They are treated as sub-mappings (or dictionaries, or data structures) within the root mapping. Suppose that a user defines the following parameters. 1"/rgb/r":255 2"/rgb/g":140 3"/rgb/b":105 Whenever a user accesses, e.g., /rgb/r , they would get back 255. But if a node tries to read the top-level /rgb name, the Parameter Server returns the whole mapping, i.e., 1{"r":255,"g":140,"b":105} Managing Time Time and durations are central aspects to the design and implementation of cyber-physical systems. For instance, a common approach to programming ROS nodes is to set the node’s main loop at a fixed rate. This ensures that publishers always produce a relatively steady stream of messages, and also has the potential to serve as a heartbeat mechanism, to ensure that the node is continuously making progress. Thus, ROS provides a few convenience classes in the client libraries to ease the management of time, durations and rates, namely: •ros::Time to represent a moment, an instant in time, such as the current time; •ros::Duration to represent a period of time, such as a period of 10 seconds; •ros::Rate a convenience to represent a fixed rate, and making a best effort at keeping it by accounting for the time used to do work in a loop. These time primitives are all based on a Time Server – an internal ROS entity that, by default, keeps track of time as any normal clock would. However, this behaviour can be changed. It is useful to change this behaviour in simulation, for instance, either to slow down the passage of time, or to speed it up. For such cases where real time is needed, though, even if running in simulation, ROS provides a wall variant of all primitives above, that bypass the behaviour of the time server – i.e., ros::WallTime , ros::WallDuration and ros::WallRate. Listing 2.9 illustrates the basic interface and usage of the time primitives. 2.3. ROS in Practice 28 4. Lesire et al. [ 106 ] propose a specification DSL that allows runtime verification of Past-time Linear Temporal Logic properties with real-time constraints; this approach is benchmarked against DeRoS, and found to be more effective and more efficient. Finally, in [ 170 ] the authors tackle a different problem: the reconstruction and consistency checking of the ROS computation graph. This approach is mixed, in that it uses static analysis for launch files – to determine which nodes make up the system – and dynamic analysis to extract the interfaces of the nodes themselves. Nodes are executed within a sandbox environment that also loads a library that intercepts calls to the ROS Master. From these intercepted calls, they are able to determine which topics and services are advertised and used by each node, and thus are able to put together the whole graph. The main disadvantages of this approach are the assumption of a standard node life cycle (i.e., all topics and services are created at setup), and, given that it is based on dynamic analysis, it can only extract information from a single execution trace. 2.3 ROS in Practice To push the quality of ROS systems forward, advanced analysis tools are undoubtedly required. Static analysis, in particular, seems to be a promising approach, despite being generally hard to implement. It is suitable for all systems and components, new and existing ones, as long as the source code is available. In an open source ecosystem such as ROS, generic components tend to be reused, and application-specific components tend to be custom made; in both cases, source code availability should not be an issue. Besides, the ROS community is large and diverse, and many roboticists are not well-versed in formal methods or standard software engineering practices, such as Model-driven Software Development, despite the number of proposed approaches for either [ 9 , 36 , 39 , 78 , 99 , 108 , 121 , 169 , 172 ]. This leads to a development process with little to no modelling and jumping straight into coding – an approach that favours static analysis. Building powerful, ROS-specific static analyses is possible [ 156 , 170 ] but far from trivial. A first challenge is that a ROS system is completely open. I.e., there is no real concept of application, since a group of nodes could operate on their own in one context, or represent just a subsystem in another context. A second challenge, as we can see in Section 2.1, is that ROS allows a high degree of freedom when it comes to system design, making it difficult to reverse engineer the computation graph. In particular, launch files are customisable with, e.g., environment variables or conditional statements. As a third challenge, the ROS client libraries also provide a myriad of primitives , used to create topics and services or to read and write parameters, that can be called at any point in the program. Our first contribution is, thus, an empirical study, published in [ 149 ], with the goal of detecting common usage patterns of ROS features and primitives, both in launch files and in the source code. The main outcome of this study is a ranking of the most frequent usage patterns, making it easier to identify where new analysis tools need to invest their effort. To address our first challenge, and for the purposes of this study, we consider a ROS application to be a top-level launch file, i.e., a launch file that is not directly 2.3. ROS in Practice 29 or indirectly included by any other launch file in the corpus. Thus, we conduct the study, driven by the following research questions. RQ1 Which ROS communication primitives are actually used, and how commonly? RQ2 In which context are these primitives used and how are their arguments defined? RQ3 What kind of features are typically used in ROS launch files to deploy applications? RQ4 How and how commonly is the ROS parameter server used? RQ5 How commonly are custom message and service types used in ROS communications? From a code quality and analysis standpoint, the answers to these questions dictate how knowledgeable static analysis (and the respective developers) must be. Knowing which primitives are used more often can help prioritise their support in tools. For static analysis, it is also very relevant to know in which context such primitives appear (namely, whether they are within control flow) and how are they parameterised (literal arguments versus variable arguments). In particular, analyses become complex, if not impossible, when values originate from the ROS parameter server. Parameters are dynamic by definition, but, contrary to regular dynamic variables (which can be altered at various points within the same process), ROS parameters can also change, without notice, by action of other processes in the network. There are only a few scenarios in which one can determine, statically, the value of a ROS parameter, e.g., when it is undefined or when it is defined in a launch file and no nodes redefine the value at any point. Finally, the usage and definition of non-standard message types limits the domain-specific knowledge tools can leverage. For example, the previously mentioned Phricky Units [ 133 , 134 , 135 ] is a tool that automatically identifies dimensional inconsistencies in ROS code. To do so, it relies on a mapping of physical units that are expected for certain fields of standard ROS messages. The introduction of non-standard message types, naturally, limits its usefulness and capability to act. 2.3.1 Corpus of the Study To put together a corpus of ROS packages would seem straightforward, at first glance. Given that ROS is deeply rooted in the world of open source software, a corpus could be as simple (and as vast) as any freely available ROS package. For instance, given that we worked with the ROS Indigo Igloo distribution, our starting point could be to traverse the distribution’s index and collect all indexed packages. However, this is an empirical study, backed by automatic mining tools, on the expected practices in standard ROS application development – and here we hit a few issues that have us trim down the corpus significantly. First, and foremost, the corpus should be representative of actual ROS systems . We focus on packages that provide building blocks for robotic applications, i.e., controllers, drivers, planners, etc.. More specifically, we chose packages from robot systems that are indexed in either the ROS Indigo Igloo or the ROS-Industrial repositories (the latter is not a subset of the former), mostly based on popularity within the community and 2.3. ROS in Practice 30 source code availability. Examples include the TurtleBot2, or the Fraunhofer IPA Care-O-bot 16 . But not all robots are equally interesting to study; some have most of their functionality confined to proprietary, ROS-agnostic drivers, exposing only a small ROS wrapper for integration purposes. Ideal systems, such as the two aforementioned examples, have most of their source built for ROS and with ROS. Our initial package corpus, based on concrete robotic systems, was then refined. Some packages are just wrappers for ROS-agnostic libraries and utilities, their purpose being to streamline the process of managing dependencies and making said utilities easily available for ROS developers. Such packages should be avoided because they do not contain any ROS nodes or primitives. Including them would: (i) skew the results (e.g., percentages relative to all packages); (ii) increase the overall time needed to process all source code; and (iii) answer none of our research questions. Moreover, we must take automation and technical limitations into account . At the time this study was conducted, our prototype mining tools were limited to parsers for launch files and C ++ source code. Consequently, any components written in other languages (with Python being the most common alternative) have to be left out of the analysis. The C ++ mining tool relies on the Clang compiler, and most ROS packages default to compiling with GCC. We had to ensure that every package could be properly compiled beforehand, which means that, in some cases, we had to make changes to the source (mostly limited to CMake files) in order to solve incompatibilities. This is an additional layer of manual work that severely hinders our capacity to process a large corpus. The initial selection yielded 480 packages. After filtering the selection, by removing metapackages and some ROS-agnostic libraries, we settled on a corpus composed of 380 indexed packages. As per our definition of ROS application within this study (a top-level launch file), the corpus contains 365 launchable applications. Table 1shows how the different packages and applications are distributed among the various robot systems17. In this table, the entry Other Packages denotes packages that are used by one or more robots, but are not part of any system in particular, such as ROS implementations of certain hardware communication protocols. Overall, 175 out of 380 packages, 46.05% of the corpus, contain C ++ source code, and are, thus, subject to the analysis pertaining to ROS primitives. In total, these represent 3,377 C ++ files. The analysis of launch file features is performed on 200 packages (52.63% of the 380) containing 901 files. By comparison, the full ROS Indigo Igloo distribution index contains 2106 packages. After excluding 294 metapackages, we found that 907 (50.06%) contain C ++ source code and 757 (41.78%) contain launch files. In relative terms, our corpus seems to be a representative sample of the ecosystem. A preliminary analysis of our corpus shows that 40.51% of all launch files (365 in 901) fall into our definition of launchable application. Unsurprisingly, we found that the package-application relation is many-to-many, i.e., a single application depends on multiple packages, and a single package can contain multiple applications. 16 https://www.care-o-bot.de/en.html 17 Some inconsistencies and unclear aspects were detected in this data after publishing the study. Here we present the correct values. 2.3. ROS in Practice 31 Name Packages Applications C++ LOC Aubo 11 9 4,893 Clearpath Grizzly 9 14 1,510 Fraunhofer IPA Care-O-bot 68 27 43,765 Kinova MICO 5 5 4,265 Robotiq Adaptive Gripper 14 3 3,294 Robotnik AGVS 8 9 2,113 Robotnik GUARDIAN 10 19 5,555 Robotnik RB-1 13 23 525 Robotnik RBCAR 9 11 933 Robotnik SUMMIT 13 7 2,837 Shadow Dexterous Hand 57 43 33,983 TurtleBot2 71 101 38,739 Universal Robot 9 19 1,418 Yaskawa Motoman 10 29 8,747 Other Packages 73 46 543,776 380 365 696,353 Table 1: Corpus of packages used for the empirical study. The collected data set, relative to the analyses over C ++ and launch files, is available online 18 . We describe the main results of the study and answer our research questions in the following subsections. 2.3.2 RQ1 – Which ROS communication primitives are actually used, and how commonly? This study is limited to the two default communication primitives offered in ROS, the publisher-subscriber paradigm and the client-server paradigm. Other mechanisms, such as Actions, were left out entirely; they were not even counted towards the publisher-subscriber paradigm which is the foundation for their implementation. We mined the source code, looking for calls to the various ROS C ++ API functions that create publishers, subscribers, service clients or service servers. Our initial guess, from reading the ROS documentation, tutorials and other reference material, was that the publisher-subscriber paradigm would be the most common. Indeed, our findings confirm this hypothesis, as shown in Figure 8. (a) Absolute values. (b) Occurrence in packages and applications. Figure 8: Number of Publishers, Subscribers, Service Clients and Service Servers in the corpus. 18 https://github.com/git-afsantos/ros_data 2.3. ROS in Practice 32 (a) Options for Publishers. (b) Types of callback functions. Figure 9: Usage of alternative primitive overloads. We have registered a total of 379 publishers, 234 subscribers, 121 service servers and 14 service clients, as shown in Figure 8a. Combined, we have 613 uses of the publisher-subscriber paradigm, as opposed to 135 uses of the client-server paradigm. In relative terms, this means that nearly 82% of all ROS communications create publishers and subscribers. Figure 8b shows that, across our corpus, 96 out of the 175 analysed packages (54.86%) create ROS topics and 34 packages (19.43%) create ROS services. The results are similar for launchable applications; 174 applications (47.67%) create topics, but only 80 applications (21.92%) create services. The prevalence of topics is an expected result, since the publisher-subscriber paradigm allows for a greater degree of flexibility. This model is more lenient in terms of system performance, since message processing happens asynchronously, and components can be built regardless of whether there are counterparts on the other end of the topic. For instance, a node that subscribes to a topic is, in theory, perfectly functional regardless of the number of publishers on that topic. On the other hand, if a node is reliant on a service, it blocks until a server is available. Looking at the collected figures, we are also able to see that these systems produce more information than they consume. The publisher to subscriber ratio is of 1.62 calls to advertise (producers) per call to subscribe (consumer). For services, the ratio goes up to 8.64 calls to advertiseService per call to serviceClient . This discrepancy could be due to robotic systems being typically designed in pyramidal hierarchical approaches. Often, the number of low-level components is larger than the number of high-level components (e.g., drivers and low-level controllers versus trajectory planners). In addition, the former produce large amounts of information (e.g., from various sensors), to be collected and processed by higher-level components, while consuming less types of information (e.g., velocity commands). We have mentioned how most of the corpus is composed of building blocks for more complex (or custom) robotic systems, so this is likely the reason behind these ratios. We now look into the different primitive overloads provided in the ROS C++ client library in Figure 9. The chart in Figure 9a shows the usage of optional parameters for advertise , the creation of a new ROS publisher. It is evident that the default version, with no optional arguments, is the preferred choice; 92.35% of all instances fall into this category. Only 20 publishers latch messages – the automatic re-publication of the last published message when a new subscriber joins the topic. This is useful for data that does not change often, like static maps, allowing a fire-and-forget type of behaviour. The other option, Subscriber 2.3. ROS in Practice 33 Status , allows the topic advertiser to define custom callback functions for when a topic subscriber joins or leaves the topic. It is a rather uncommon feature; there are only 9 advertisers that make use of it, distributed between two packages from Fraunhofer IPA Care-O-bot for image processing. The two options are not mutually exclusive, but we have found not a single topic advertiser using both at the same time. There are 11 Care-O-bot applications, for different versions of the robot, that use a combination of all types of calls to advertise. The other chart, in Figure 9b, shows the preferences of users regarding the types of callback function registered on subscribe (to create a subscriber) and on advertiseService (to create a service server). It is clear that the vast majority of callback functions are member functions (methods) of a C ++ class, with 312 functions out of 355. Other variants include global functions, with 25 instances scattered across 10 packages and 28 applications, and 18 Boost functions – a function wrapper created with the Boost C ++ library, to create closures, i.e., to bind some variables to specific values whenever the wrapped function is called. The likely reason for the dominance of member functions is to keep internal state from one function call to the other, or to easily share state between different program points, or even threads. Global functions are disfavoured in this case, since they would either be stateless, or have to rely on global variables to share state (a discouraged practice, in general). Boost functions are a rather uncommon middle ground alternative, that, most of the time, can be replaced with the simpler member function. As a last remark, we have registered no occurrences of any ROS primitive using a transport protocol other than TCP, which is the default. 2.3.3 RQ2 – In which context are these primitives used and how are their arguments defined? This research question is more closely tied to the required complexity of static analysis tools. In terms of context, we want to assess whether primitives are always called from the main control flow path, or whether there might be primitives called conditionally, or even within loops. Analyses step up in complexity when there are dynamic conditions involved, as the structure of the ROS interface is no longer static. A similar reasoning applies to the arguments supplied to primitives, such as topic names and message queue sizes. If the arguments are literal values, defined on the spot, not only is the source code more readable but implementing a precise static analysis tool also becomes much more accessible. If, on the other hand, the arguments stem from dynamic variables (or function calls, even), sophisticated data flow and control flow analyses become a requirement. We cannot have accurate data on the distribution of primitives under control flow constructs, relying solely on automated mining methods. To gather accurate numbers, we would require a full-fledged control flow analysis tool for C ++ . Building such a tool is a complex and daunting task, and one of the aims of this research question is precisely to understand whether such an endeavour is worth the time it requires. So, with this chicken and egg problem on hands, we settled for a middle-ground approach. We have only accounted for control flow constructs, e.g., if or for , within the same function as the primitive; we did not perform a full control flow analysis of the entire program. With this limitation in mind, we have found that the number of conditional primitives is rather low, as shown in Figure 10a, amounting only to 74 out of 2.3. ROS in Practice 34 748 primitives (about 10.43%). This seems like a rather promising figure for static analysis tools, if the actual numbers, when considering the control flow of the entire program, are not much higher. (a) Absolute values. (b) Occurrence in packages and applications. Figure 10: Distribution of primitives under control flow. In terms of packages, as shown in Figure 10b, we have found 19 packages (10.86%) that use conditional publishers or subscribers, while only 2 packages (1.14%) use conditional services. One of these packages belongs to Yaskawa Motoman, in which services are advertised whithin a loop, and another belongs to Aubo, in which a service is created if the driver initialises successfully. Also in Figure 10b, we can see that nearly one third of all applications (111, 30.41%) use conditional topics, and 64 applications (17.53%) use conditional services. Considering how few packages use these features, here we can see just how often different applications reuse the same packages. The analysis of argument types is shown in Figure 11. This time, we consider not only the arguments for communication primitives, but also for the ROS time primitives. We studied ROS names (both for topic and services), message queue sizes and time amounts for ros::Time , ros::Duration , ros::Rate and their Wall variants. The time primitives are relevant, for instance, to perform analyses related to publishing rates, as in [156]. Figure 11: Types of arguments for various ROS primitives. The results show that, for ROS names and queue sizes, the vast majority of arguments is defined as literal values: 556 out of 748 ROS names (74.33%) and 607 out of 613 message queue sizes (99.02%) are literals. For the remaining arguments, we can see that 149 names and 6 queue sizes result from reading variables, and yet 43 names result from other expressions (e.g., string concatenation, function calls, etc.). 2.3. ROS in Practice 35 Non-literals can be found in 36 packages (20.57%) and 150 applications (41.10%). The figures for the time primitives are much more balanced. Only 53 out of 105 primitives are created from literal values (50.48%), while 43 are created from the values of variables and the remaining 9 come from other sources. Non-literal time values can be found in 29 packages (16.57%) and 88 applications (24.11%). Further inspection of the argument values shows a few interesting facts. Among the literal values for ROS names, we looked for the presence of global ROS names. Their use is discouraged, in general, as it makes components less reusable. We registered 38 publishers, 40 subscribers and 4 service servers that use global names, for a total of 82 names out of 748 (10.96%). They were found in 23 packages (13.14%) and 61 applications (16.71%). Among the literal values for queue sizes, we registered 9 instances of unbounded queues (a highly discouraged practice) and a surprising 331 queues of size 1 (about 54%). While singleton queues are not harmful per se, they are worthy of notice and further thought. Singleton queues should only be used when there is no interest in processing all messages, but rather only the most recent ones, since ROS discards the oldest messages when a queue is full. Judging by the message types associated with the majority of these occurrences, we can estimate that singleton queues tend to be used for control messages (e.g., teleoperation commands) or highly volatile data (e.g., sensor data, especially camera related). 2.3.4 RQ3 – What kind of features are typically used in ROS launch files to deploy applications? As described in Section 2.1, launch files are XML files with a specific set of tags and attributes. Launch files are interpreted, often with the roslaunch tool, and have their own semantics. Building an analysis tool that understands the whole launch file language is not overly complex, as the language itself is not very extensive. However, it still poses a few challenges, such as dynamic, external variables (e.g., environment variables) and conditionals. By measuring the use of the various tags and attributes of a launch file we can gain insight on how relevant each feature is, and how systems are deployed in practice. Note that, for the purposes of this study, we focus on launchable applications, as previously defined, rather than individual launch files. We consider applications in their entirety; <include> tags are resolved, so that we can analyse systems as they are deployed in practice. This means that the contents of any launch files that are included multiple times will be counted multiple times as well. Our corpus contains 365 top-level launch files, and 901 launch files in total. The primary use of launch files – and, consequently, of applications – is to deploy nodes, so we start our analysis with the <node> tag and the chart in Figure 12. Overall, we registered a total of 1418 nodes, of which only 275 (19.39%) are unique. Such a low number is the result of compositional construction of applications. We have 901 launch files in total, but only 365 are top-level ones; this means that many launch files are reused as parts of a larger system, and thus, any nodes they launch end up repeating (possibly with different parameters) over various applications. Nodelets are seldom used, amounting to 119 out of the 1418 nodes. Besides being a relatively niche feature, they are also mostly used in the TurtleBot2, a system with 101 top-level launch files and 90 uses 2.3. ROS in Practice 36 Figure 12: Uses of the <node> tag. of nodelets in total. Out of the remaining 29 nodelets, 26 belong to three applications of the Fraunhofer IPA Care-O-bot system, and 3 belong to an application of the Clearpath Grizzly. The most notable among the remaining node features are, perhaps, the use of custom command-line arguments, used in 554 nodes (39.07%), and marking nodes as able to respawn , used in 560 nodes (39.49%). To be able to respawn means that if the node terminates, for any reason, a new copy is started automatically, until the ROS system as a whole is shut down. Other node-related features are not really common. Only 46 nodes are marked as required , meaning that if the node terminates the whole launch application should be brought down. We also registered 201 conditional nodes, i.e., nodes under a conditional statement within a launch file, and 16 remote nodes, nodes that are launched on a machine specified by its network address that is (possibly) different from the one interpreting the launch file. Figure 13: Overall use of launch file features. The chart of Figure 13 shows the overall usage of other launch file tags and features within applications. Immediately, we are able to see that the use of the <arg> tag, whose purpose is to define local variables within a launch file, is commonplace with 4085 registered uses. A large number of these, 2069 to be precise, is used to pass along to <include> tags, i.e., variables defined at a high level to pass to lower-level launch files. As for the <include> tag, we observed 1015 instances. Both of the tags related to the ROS parameter server, <param> and <rosparam> , are also abundantly used, with 2675 uses and 1060 uses, respectively. Other frequently used features of launch files are remappings (1009 instances), reading environment variables (652 instances), and conditional tags (1179 instances). In contrast, the <machine> 2.3. ROS in Practice 37 tag, used to define or reference other machines within the network, is seldom used, with only 46 instances. Four of these appear on the Shadow Dexterous Hand system, and the remaining 42 are part of Fraunhofer IPA Care-O-bot applications. Based on the observed figures, we can estimate that, on average, each launchable application remaps between two and three names, reads about two environment variables, and declares over three entities conditionally. There are implications from these statistics, as these features require additional analysis steps. For remappings, tools are likely forced to implement the same name resolution mechanisms that ROS uses. For environment variables, either user input is required (no automation) or the analysis has to take place in the same environment where the launch file is meant to be used (reduced portability). For conditionals, tools have to resolve arbitrary values, which may come, e.g., from environment variables. 2.3.5 RQ4 – How and how commonly is the ROS parameter server used? The previous research question already sheds some light on how commonly the parameter server is used in the context of ROS applications (see Figure 13). Namely, the simpler <param> tag is used 2675 times, while the more complex <rosparam> tag is used 1060 times. On average, this amounts to over 10 parameters per application, if we took each tag to be equivalent to one parameter. However, in some contexts, either tag can define multiple parameters at once, so the actual number is likely much higher. In addition, out of all 3735 parameter-related tags, we observed that 978 (26.18%) define parameters from the contents of YAML data files, and 240 (6.43%) define parameters from the printed output of command-line programs. In summary, there are 2517 parameter tags whose effects are more or less immediate, while nearly one third of the tags is not self-contained within the launch files. These tags are scattered among 232 out of the 365 applications, meaning that nearly two thirds of all applications (63.56%) use the ROS parameter server. Regarding the use of the parameter server by the nodes, we have not found any surprises. As stated in Section 2.1, the parameter server is not designed for high performance, meaning that it should only provide access to static data. We found only 38 runtime write operations, compared to 705 readings. Out of these read operations, 585 (82.98%) declare a default value for when the parameter is not defined in the server, as a fallback behaviour. Most of the accessed names (666) are given as literal arguments too, which makes analysis easier. Overall, we can find accesses to the ROS parameter server in 87 out of 175 packages with C++ source code (49.71%). Do note, however, that we have limited the study to the basic getParam and setParam variants of the ROS C ++ client libraries. There are many means of indirectly using and defining parameters (e.g., with the dynamic_reconfigure package) that are beyond the scope of this study. 2.3.6 RQ5 – How commonly are custom message and service types used in ROS communications? Defining new ROS message and service types is not overly common, although it is sometimes necessary. We have found that 74 out of the 380 packages in the corpus (19.47%) define new types. More specifically, 3.1. State of the Art 44 Lastly, there is also existing work applied to ROS, still with a pure static analysis approach [ 127 , 142 , 156 ], as presented in Section 2.2. The first published approach [ 142 ] extracts the publisher and subscriber part of the ROS computation graph, from the source code of C ++ nodes. The extraction process traverses the source code and identifies function calls to the various ROS primitives (e.g., advertise ). Each call is annotated with control flow information, i.e., conditions that might affect it. It further distinguishes reactive and proactive message publications by tracing back calls to publish until it finds a callback function (in which case the publication is reactive) or a leaf node in the source tree (e.g., the main function, in which case it is proactive). The second approach [ 156 ] also focuses on the publisher-subscriber aspect of the computation graph, but the model is enriched with launch file information, such as remappings. Similarly to how the previous approach classifies message publications as reactive or proactive, this approach classifies publishers as dependent or independent. The main goal is to conduct rate impact analysis – i.e., to determine the impact of changing a single node, especially with respect to its publication frequency. The naïve stance would be to assume that all nodes transitively reachable from the changed node would be affected, but this might not be the case. If the connected subscribers do not publish messages based on the rate of incoming messages – in other words, if publishers are rate-independent – the nodes are, in principle, not affected by the changes. A publisher is deemed to be rate-independent when it cannot be traced back to a callback function or when it is used under a fixed-rate construct (e.g., timers or loops with adaptive sleep). More recently (and published at the same time as our own approach [ 151 ]), Muscedere et al. [ 127 ] used static analysis to identify Feature Interactions . A Feature Interaction occurs when two features of a system, that work correctly on their own, intefere with one another when executed at the same time. Simply put, a feature is a high-level component that is nearly independent, e.g., a ROS node. Similar to our approach (presented in this chapter, and its implementation in Chapter 5), the proposed toolchain relies on an Abstract Syntax Tree of the C ++ ROS components to extract a database of facts (function calls, variable assignments, control flow, etc.). With the use of relational algebra transformations, they are able to infer additional facts, relative to component dependencies and information flow. Then, a query engine is used on top of the fact database to look for user-defined patterns that represent potential Feature Interactions. M i x e d A n a l y s i s Many approaches to model extraction recognise the complementary nature of static and dynamic analysis, and end up employing a combination of the two [98,120,147,157,170]. The work of Silva and Campos [ 157 ] combines static and dynamic analyses in the context of Web application GUIs. Dynamic analysis is used to crawl the interfaces, looking for user inputs (e.g., buttons and forms), and to build the initial state diagram of the application. Since JavaScript event handlers are always available on the client side, static analysis can be exploited to identify variables that lead to different state transitions from the same user action. Conditions and value combinations are then tested, until a final version of the model is achieved. Riva and Rodríguez argue that, in order to better describe and understand software architectures, multiple views of the system are necessary [ 147 ]. Their work proposes combining structural and dynamic information using a four-step iterative process. 3.1. State of the Art 45 1. Definition of architectural concepts. What is a component, and how do components communicate? 2. Data gathering from various sources. Employ both static and dynamic analysis. Also make use of available documentation and expert knowledge. 3. Abstraction. Transform the low-level model generated from the previous step into different highlevel, domain-specific views. A rule-based Prolog system is used to formally define model to view transformations. 4. Presentation. How to present logical, process, physical and development views of the system. Directed graphs are proposed for static views (system structure), while simplified message sequence charts are the model of choice for dynamic aspects (system behaviour). Krogmann’s PhD thesis [ 98 ] addresses the problem of reverse engineering component-based software architectures for the design and evaluation of performance properties. Krogmann states that no previous satisfying approach existed to reverse engineer behaviour and performance models for component-based software architectures, based on a language independent code analysis. Behaviour models of components need to be highly parameterised with regards to: i) changing usage (number of users, user interaction with the system, varying amounts of data); ii) changing assembly (connecting different components or different component implementations); iii) changing execution platforms (fast versus slow servers). This thesis proposes combining not only static and dynamic analyses but also statistical analysis, to achieve the reconstruction of static architectures, behaviour specification and highly parameterised, abstracted performance models of component-based software systems. Such models ultimately enable a range of reasoning and prediction techniques in: • Sizing – to estimate the necessary hardware to handle specific workloads, or to achieve a certain degree of reliability and performance; • Legacy software extension – to estimate the overall system quality after adding new components to a legacy system; • Reuse – to estimate the impact of adopting an existing component implementation; • Design optimisation – to estimate the overall performance or reliability of the system. The domain of microservice-based software is one that shares similarities with ROS. Microservices decouple network-accessible components, enhancing independent development of components, deployment and scalability. As is the case with ROS, the architectures of these systems are highly dynamic. Often they are not defined upfront, but rather emerge by dynamically assembling services into systems. This makes it hard to extract component relations from static sources and artefacts. In [ 120 ], the authors present an architecture extraction prodecure that combines static service information with infrastructure-related and aggregated runtime information for REST microservices. Architectural information is organised in three levels: 1. Service – mostly static information, such as the service API, organisational information and the domain model; 2. Infrastructure – service requirements, execution environments, deployment and scalability; 3.2. A Metamodel for ROS Applications 46 3. Interaction – observed communication among services (requests and responses) gathered from the runtime, and aggregated over long term windows. Lastly, in the domain of ROS, as presented in Section 2.2, Witte and Tichy [ 170 ] propose a process to extract the ROS computation graph that uses static analysis for launch files and dynamic analysis for node interfaces. They deem static analysis alone to be too complex, because resources can be added to the computation graph at any time, and launch files reference node executables – finding the corresponding source code is not trivial. Their approach has nodes running within a sandboxed environment which, with the help of an additional library, intercepts calls to the ROS Master, in order to build the dependencies on topics and services. However, as stated by the authors, resources can be created at any time, and their approach assumes that nodes follow a standard life cycle, in which all resources are created during set up. A general approach would have to monitor nodes indefinitely. They acknowledge this potential weakness, and propose the countermeasure of having the user provide annotations as launch file comments, to specify the missing bits of the extracted model, as seen in Listing 3.1. 1<launch> 2<node name="listener" pkg="roscpp_tutorials" type="listener"> 3<!-- <topics> 4<topic name="chatter" type="String" class="sub"/> 5</topics> --> 6</node> 7</launch> Listing 3.1: Specifying subscriber information as launch file comments [170]. 3.2 A Metamodel for ROS Applications There is no lack of research in modelling ROS systems. And with good reason, since models enable a wide variety of architectural and behavioural analysis and validation techniques. Still, we find a detrimental gap in the current state of the art. Notice how most of the existing approaches fall under (at least) one of the following categories. 1. The approach requires expert knowledge (e.g., in Formal Methods). It is not amenable to be used by a typical ROS developer. 2. Even though models are used, no metamodel is explicitly documented. 3. Some aspects of ROS are left out. 4. There are assumptions about how the concepts should be used (e.g., nodes following a specific life cycle). 5. The models only include entities from the system’s runtime (e.g., nodes and topics, but not packages and source files). The last issue, in particular, is very prominent. As described in Chapter 2, there are two sides to ROS systems: the runtime, which is mostly composed of the ROS computation graph and often tackled by other 3.2. A Metamodel for ROS Applications 47 Figure 15: Diagram notation. authors; but also the static artefacts, at the file system level, such as packages and source files. It is from the latter that nodes are built and systems are set up in the first place. A number of different analyses can take place solely at this level, even [ 52 , 139 , 148 ]. There is a whole graph of package dependencies to explore, not to mention the more intricate dependencies among source and launch files. A metamodel that is truly complete should encompass all these entities as first-class citizens, and exploit the relations between them. One of the most useful (and often disregarded) relations is traceability – identifying culprit source artefacts when a problem is encountered in a node, and vice-versa. Source artefacts and ROS runtime resources are two sides of the same coin. In this section we propose a metamodel to describe the software components of ROS systems [ 151 ] that addresses the aforementioned issues. The various key entities of this metamodel are described with a schema for YAML data representation. For readability purposes, we defer the schema’s definition to the Appendix B; in this section, we simply use examples of the schema. We further illustrate the concepts with class diagrams, where edges use the Entity-Relationship notation for cardinality, dashed boxes represent abstract entities, and solid boxes represent concrete entities. We use abstract entities for readability purposes. All abstract entities have concrete instances. We use sectioned boxes, with entity name and list of attributes, for entities defined in the current diagram. Plain boxes, just with an entity name, are used to reference entities that are defined in other diagrams. Figure 15 shows the diagram notation. The remainder of this section goes into detail about each of the entities in the metamodel. The modelled entities are split into two groups, for the source artefacts and runtime entities. Some entities and relations are constrained by rules that cannot be captured either by the schema or by the diagram notation. In these cases, we will provide textual explanation, and assume the existence of a model validation tool. Some concepts provided by libraries, such as Actions and Dynamic Reconfiguration, were left out for future extension, i.e., we do not have concrete entities in the metamodel for these features. In spite of this decision, note that these features are often implemented in terms of the basic Topic, Service and Parameter primitives – meaning that, at a risk of losing precision, the metamodel is flexible enough so that they can still be captured. 3.2. A Metamodel for ROS Applications 48 3.2.1 Source Entities A Source Entity is any entity that is static and whose purpose is to build the ROS system. They are often easily identifiable via artefacts in the file system (e.g., files and directories). We will go over familiar entities first, related to the development process itself, and then transition to the entities that are more closely tied with the ROS runtime. Source File A Source File is a single file in the file system. We assume that all files belong to a single ROS package, i.e., there are no orphan files. Files are characterised by their name (a relative path within their package) and their language . The language of the source file is one of: C ++ ( cpp ), Python ( python ), Package XML ( package ), Launch File ( launch ), CMake ( cmake ), ROS Message ( msg ), ROS Service ( srv ), ROS Action ( action ), or unknown for unspecified or unknown languages. These are the most common alternatives, but it is trivial to extend this enumeration to allow, e.g., JavaScript, which in recent years has also seen some application in ROS. Figure 16: Class diagram for Source Files. Optionally, each file can provide its own source tree , an Abstract Syntax Tree under some standard or convention, whose details are not part of this metamodel. Lastly, files can specify a set of dependencies on other files. For instance, C ++ source files depend on the header files they #include , Python scripts depend on all scripts they import and launch files depend on other launch files that they <include> . Figure 16 shows the class diagram for Source Files. Listing 3.2 shows the YAML specification, according to the metamodel schema, for the manifest file of the fictibot_drivers package, from our Fictibot running example. 1name:"package.xml" 2package:"fictibot_drivers" 3language:"package" 4source_tree: null 5dependencies: [] Listing 3.2: YAML specification of a Source File. Package A Package is an abstraction for a ROS Package. One of the mandatory characteristics of packages is that they must contain the package XML manifest file. From this file, we can gather a few metadata, such as the set of authors and maintainers , the version number, dependencies on other packages, the file system path and whether it is a metapackage (Figure 17). While most of this information 3.2. A Metamodel for ROS Applications 49 is not crucial for most kinds of analyses, it can be helpful, for instance, to assign issues, or to record evolution over time (via version numbers). Figure 17: Class diagram for ROS Packages. We assume that each package belongs to a project , may be part of a repository , and can build any number of ROS nodes . Since the names of files are relative paths within a Package, it follows that no two files within the same Package can have the same name . Uniqueness of the file names is enforced in the schema. Listing 3.3 shows schematic YAML for the fictibot_drivers package. 1name:"fictibot_drivers" 2authors: {name:"André Santos",email:"[email protected]"} 3maintainers: {name:"André Santos",email:"[email protected]"} 4version:"0.1.0" 5path:"/home/ros/ws/src/haros_tutorials/fictibot_drivers" 6is_metapackage: false 7dependencies: ["roscpp","std_msgs"] 8project:"Fictibot" 9repository:"haros_tutorials" 10 nodes: ["fictibot_driver"] 11 files: 12 -"package.xml" 13 -"CMakeLists.txt" 14 -"include/fictibot_drivers/motor_manager.h" 15 -"include/fictibot_drivers/sensor_manager.h" 16 -"src/driver_node.cpp" 17 -"src/motor_manager.cpp" 18 -"src/sensor_manager.cpp" Listing 3.3: YAML specification of a Package. Repository A Repository is a standard source code repository. As seen in Figure 18, it is characterised by its name , version control system ( vcs , e.g., git or svn ), its file system path and its version (e.g., branch name in git ). Optionally, not shown in the figure, metadata such as the number of commits, contributors, the repository’s URL or the issue tracker can also be appended. An implicit rule, not captured by the schema, is that the path of every Package under a Repository must be a (direct or indirect) child path of the Repository’s path. While repositories are not a core, or necessary, concept in ROS, they are a natural part of software development. Including them in the metamodel enables, for instance, gathering process metrics (commits 3.2. A Metamodel for ROS Applications 50 Figure 18: Class diagram for Repositories. and contributors) as well as refining traceability, and possibly pointing issues directly to an issue tracker. It also aids in tracking evolution over different versions. Listing 3.4 shows schematic YAML for the haros_tutorials repository3, the repository that contains the Fictibot packages. 1name:"haros_tutorials" 2vcs:"git" 3version:"master" 4path:"/home/ros/ws/src/haros_tutorials" 5packages: 6-"fictibot_drivers" 7-"fictibot_controller" 8-"fictibot_msgs" 9-"fictibot_multiplex" Listing 3.4: YAML specification of a Repository. Project A Project , like a Repository, is a concept that is not directly introduced in the ROS documentation, even though it exists (implicitly or explicitly) in practice. The main purpose of this entity is to aggregate a set of packages that should be part of the same logical unit, such as a robot with a specific application. Projects are not partitions of packages. There can be multiple projects using the same packages, although probably with different configurations. There can only be one project per model – the project is the main entity (and entry point) of the whole model. Figure 19: Class diagram for a ROS Project. As seen in Figure 19 and Listing 3.5, besides containing a set of packages , a project may also contain a set of configurations (a runtime entity). Thus, along with Nodes (as we will see), Projects are a bridge between source and runtime entities. N o d e The term Node in ROS is actually a bit ambiguous, as it can mean one of two things. It could be a node in the computation graph, a process interacting with the system, or it could be an executable, built 3https://github.com/git-afsantos/haros_tutorials 3.2. A Metamodel for ROS Applications 51 1name:"Fictibot" 2packages: 3-"fictibot_drivers" 4-"fictibot_controller" 5-"fictibot_msgs" 6-"fictibot_multiplex" 7configurations: ["minimal"] Listing 3.5: YAML specification of a Project. from source code, from which the runtime nodes are instantiated. In this metamodel, Node means the latter. We use Node Instance for the former. Figure 20: Class diagram for a ROS Node. As seen in Figure 20, a node is identified by its executable name , always belongs to a package and enumerates the source files needed to build it (that, in most cases, belong to the same package). The model should also tell whether the node can be loaded as a nodelet . Optionally, as is the case with source files, the node may contain the full source tree of the code that builds it, i.e., a merging of the source trees from all source files. Properties are textual properties about the Node’s behaviour. The syntax and semantics of the specification language are given in Chapter 4. This is one of the entities (along with Project) that provides a direct connection to the runtime view, via instances , which is the set of all Node Instances created from a particular node. If available, nodes also provide the ROS name that is used by default to identify the node, when launch files do not override it at instantiation. Finally, when possible, nodes should list all calls to ROS primitives throughout their code, i.e., all calls to the ROS interface that would create or use topics ( advertise and subscribe ), services ( advertise service and service client ) and parameters ( get parameter and set parameter ). Listing 3.6 shows an excerpt of schematic YAML for a Node specification. We do not include the full listing, since including all calls to the ROS primitives would impact readability. ROS Primitive Call A Primitive Call is a function call to any of the ROS functions that create or make use of a resource, such as advertise that is used to create a topic publisher. As seen in Figure 21, 3.2. A Metamodel for ROS Applications 52 1name:"fictibot_driver" 2package:"fictibot_drivers" 3is_nodelet: false 4ros_name:"fictibot_driver" 5files: ["src/driver_node.cpp","src/sensor_manager.cpp","src/motor_manager.cpp"] 6advertise: 7-name:"bumper" 8type:"std_msgs/Int8" 9queue_size: 21 10 latched: false 11 traceability: 12 package:"fictibot_drivers" 13 file:"src/sensor_manager.cpp" 14 line: 10 15 column: 29 Listing 3.6: YAML specification of a Node (excerpt). some attributes and relations are similar between all types of primitives (although the names of the attributes change), but the model still treats each primitive type as its own entity, so that it is more easily extensible. Figure 21: Class diagram for ROS Primitive Calls. All primitives have a resource ROS name (e.g., the topic name given to a call of advertise , before applying any remappings) and a value type (e.g., the message type for topics). In addition, all primitives have a source code location, and possibly the control flow paths containing dynamic conditions. Primitives can be instantitated as links , a runtime entity of this metamodel. The Advertise and Subscribe primitives track the message queue size . Lastly, the Parameter primitives track default values (when reading and the parameter is not defined) and written values. Listing 3.6 already includes an example of an Advertise call in schematic YAML. S o u r c e C o n d i t i o n a n d S o u r c e L o c a t i o n While not really entities per se, Source Conditions and Source Locations (Figure 22) are useful complex attributes that some other entities require. 3.2. A Metamodel for ROS Applications 53 Source locations point to specific locations in the source code, describing a package name, a file name, a line number and a column number. Figure 22: Class diagram for Source Condition and Source Location. Source conditions are used to store dynamic conditions (as in the condition of an if or for statement) that might affect whether another entity is evaluated. They are essentially an extension to the source location, adding the type of statement and a string with the concrete expression . Multiple conditions can be grouped under a control flow path . 3.2.2 Runtime Entities A Runtime Entity , in contrast to Source Entities, is an entity that is dynamic, and generally only exists while a ROS system is in operation. These are also some of the most iconic concepts in ROS, including node instances, topics, and the computation graph in general. Many runtime entities are Resources of the computation graph. A notable exception is the Configuration concept that we introduce as an abstraction for a ROS application, and as a slight extension of the computation graph. Every resource, as presented in Chapter 2, has a ROS name that should be a unique identifier among the same class of resources. I.e., although not encouraged, a topic, a service and a parameter can all have the same ROS name. Two different topics sharing the same name, however, is not possible. In addition, every resource belongs to a single configuration , and might be considered conditional (i.e., it is not always part of the configuration). In that case, the resource should provide the control flow graph of dynamic conditions on which it depends. These may come either from source or launch files, depending on the case. Node Instance A Node Instance is the runtime counterpart to the source entity Node . While the Node represents the executable file in the file system, the Node Instance represents a process spawned from a Node. It is a resource in the ROS computation graph. As seen in Figure 23, besides including a reference to the original node executable, a Node Instance also provides the command line arguments given at launch to the executable and a table of remappings. Being a spawned process, its presence in the final Computation Graph might depend on a number of conditions , such as the conditional statements of a launch file. All ROS Primitive Calls in the original node are instantiated as ROS Links ( publishers , subscribers , servers , clients , getters , setters ). During this step, the namespace and remappings of the node instance are applied to the arguments of the primitives, yielding, thus, the concrete links. Listing 3.7 shows an excerpt of schematic YAML for a node instance. 3.3. Model Extraction 60 1int main(int argc, char **argv) { 2ros::init(argc, argv, "fictibot_controller"); 3ros::NodeHandle n; 4RandomController controller(n, 10 /*Hz*/); 5ros::Rate loop_rate(10 /*Hz*/); 6while (ros::ok()) { 7controller.spin(); 8loop_rate.sleep(); 9} 10 return 0; 11 } Listing 3.11: The main function of the src/controller_node.cpp file. Note that searching for Nodes the other way around, i.e., starting with the parsing and look up of the init function in source code files, is not an optimal solution for a few reasons. • The call to ros::init or rospy.init does not necessarily occur in the main file of the program, although it is often one of the first instructions of the main function. • Identifying the file with this function call, in C ++ , might not suffice to identify all files that compose the node. One might be able to trace back header files, via #include directives, but other implementation files still require the full compile command (as given in CMake). • Although unlikely, the same file with a call to ros::init or rospy.init might be reused to compile multiple (different) nodes, e.g., by retaining the same header files but changing the implementation files in C ++ . This could be used to produce similar nodes for different target hardware, or to distinguish between hardware and simulation nodes. 3.3.3 ROS Primitive Calls When a node is identified, during the extract_nodes_and_primitives step, the set of source files that build it is also known, as seen with add_executable . These files must be parsed in order to extract the calls to ROS primitives, and this is the first true obstacle to static analysis. It is easy to understand that resolving all arguments of a primitive call to concrete values might be hard, or even impossible in some cases. But, sometimes, especially when layers of indirection come into play, detecting the primitives themselves could be the problem. For instance, calling functions dynamically (e.g., with function pointers) or using wrappers provided by libraries, such as the ROS message_filters or dynamic_reconfigure packages, adds complexity to the process. The latter is especially prominent in practice, as we can see in the evaluation chapter (Chapter 8). Fortunately, as suggested by our empirical study [ 149 ] (see Section 2.3), most occurrences are rather simple to process, in terms of their arguments, at least, with the majority being literals. However, the ROS client libraries provide multiple overloads for the same primitives. In the C ++ client library, for example, there are 3 overloads for advertise – which is one of the primitives with the fewest overloads. Thus, parsing primitive calls is not a matter of identifying one call of each type, but rather a roster of calls per 3.3. Model Extraction 61 primitive. Ensuring that this catalogue is exhaustive (possibly including popular libraries as well) is key to ensuring the precision and recall of the extraction process. When it is not possible to fully determine the argument ROS name (i.e., the topic, service or parameter name), the extraction process should still resolve as many parts of the name as possible. For instance, it might be the case that the namespace is known, but not the resource’s own name, or vice-versa. Unresolved parts of the name are replaced with a wildcard ? , in an effort to make the model as complete as possible, and enabling posterior analysis or user intervention to refine the names. Another non-trivial detail of this step is how to deal with conditions. A simple implementation would only look at the control flow of the function containing the primitive call (as we did for the empirical study in Section 2.3), while a more thorough analysis would traverse all possible program paths that lead to the primitive call. Within the boundaries of static analysis, we strive for the latter. That is, if the current function body does not provide enough information (e.g., because a variable is a function parameter), we traverse the bodies of the functions that call the current function, and so on, effectively traversing as many program paths as possible, but in reverse order. 3.3.4 Configurations and Resources After identifying all the source artefacts and calls to the ROS primitives, the reconstruction of the computation graph can begin ( extract_configurations , Listing 3.12). As mentioned before, there is no way to know, for certain and in advance, which components are part of an application and which applications are part of a project. Thus, we resort to user input. At the bare minimum, a configuration specification provides the name of the configuration and the list of launch commands that compose the application. It is a list of commands, and not a set, because the order in which nodes are launched and parameters are set could be relevant (i.e., implicit dependencies between launch files). 1def extract_configurations(config_specs, P, F, N): 2C = [] 3for name, data in config_specs.items(): 4configuration = Configuration(name) 5for item in data["launch_commands"]: 6command = item["command"] 7args = item["args"] 8if command == "roslaunch": 9add_roslaunch(configuration, args, P, F, N) 10 elif command == "rosrun": 11 add_rosrun(configuration, args, N) 12 hints = data.get("hints") 13 apply_hints(configuration, hints) 14 configuration.properties = data.get("properties", []) 15 C.append(configuration) 16 return C Listing 3.12: Overview of the configuration construction algorithm. 3.3. Model Extraction 62 To build a configuration, each launch command is interpreted in order. Launching individual nodes is relatively straightforward; the challenge resides on launch files. For each launch file, the algorithm has to mimic the behaviour of roslaunch , the utility that interprets launch files and deploys systems. That is, it must keep the semantics of all launch tags: <remap> tags must apply to the correct nodes; <node> tags are processed in the order they appear, but cannot make assumptions about which nodes are actually launched first; <param> tags must create parameters within the correct context (i.e., globally, or under a node’s namespace); etc. This step can introduce various unresolved conditions and wildcards, due to conditional statements present in the launch files, or simply due to arguments provided via command line (manually, by the user), at launch. Parsing launch files allows us to build all Node Instance and Parameter models, and from the pkg and type attributes of <node> tags we know which Node models correspond to each Node Instance. For instance, the launch/multiplexer.launch file of fictibot_controller , in Listing 3.13, contains 3 <node> tags, which correspond to 3 Node Instances. Only the ficticontrol node is affected by the <remap> tags. 1<launch> 2<node name="fictibase" pkg="fictibot_drivers" type="fictibot_driver" /> 3<node name="fictiplex" pkg="fictibot_multiplex" type="fictibot_multiplex" /> 4<node name="ficticontrol" pkg="fictibot_controller" type="fictibot_controller"> 5<remap from="controller_cmd" to="normal_priority_cmd" /> 6<remap from="/stop_cmd" to="normal_priority_stop" /> 7</node> 8</launch> Listing 3.13: The fictibot_controller launch/multiplexer.launch file. The last fully automatic step is, for each Node Instance, to build ROS Links from the ROS primitive calls of the corresponding Node model. Links inherit most of their attributes directly from primitive calls, with the notable exception of the ROS resource name. The resource name is resolved using the name resolution rules of ROS, the name and namespace of the concrete Node Instance, as well as its remappings – with the exception of also allowing the wildcards introduced in the extraction process. Whenever the name resolution yields a name that is not yet present in the configuration, a new resource (Topic, Service or Parameter) is created and added to the graph. After creating a new resource, or retrieving an existing one with the same name, the new link is finally created between the node and the target resource. For instance, in Fictibot’s Controller the primitive calls indicate topic advertisements for /controller_cmd and /stop_cmd (Listing 3.14), but, with the remappings of the previous launch file, the corresponding links would be created to /normal_priority_cmd and /normal_priority_stop instead. 1RandomController::RandomController(ros::NodeHandle& n, double hz) { 2/* ... */ 3command_publisher_ = n.advertise<std_msgs::Float64>("controller_cmd", 1); 4stop_publisher_ = n.advertise<std_msgs::Empty>("/stop_cmd", 0); 5/* ... */ 6} Listing 3.14: Some of the topics used in the src/random_controller.cpp file of fictibot_controller. 3.3. Model Extraction 63 3.3.5 User-provided Hints In many cases, the model should be complete after the previous instantiation step. Depending on the precision and recall of the implementation, as well as the source code under analysis (which could have a large number of dynamic values), the resulting model could end up featuring many unresolved names. To accomodate for this, we extend the YAML configuration specifications, provided as user input, to also include optional extraction hints (apply_hints in Listing 3.12). Hints are, in essence, partial models built by hand, with varying levels of detail. They are specified per configuration, and they follow the same YAML schema that defines our runtime metamodel entities, for the most part. We focus on runtime entities because source entities, such as packages and files, are straightforward to extract correctly. The problem lies mostly in primitive calls, as previously explained, which are used to instantiate links. Our current approach uses hints to fix the extracted model of the runtime entities that are the prime subject for analysis, although it could be extended to allow for more entities. The major difference between extraction hints and the metamodel’s YAML schema is that each entity includes a create flag. When set to true, the entity should include its required attributes, as per the schema; the entity is meant to be created and manually added to the extracted model, in all cases. Otherwise, the only required attribute is the ROS name, as the hint is meant to fix automatically extracted entities. ROS names are used to match with extracted entities, and if there is more than one possible match – due to duplicate entities in the graph, or wildcards in the name – we resort to traceability information to resolve conflicts. That is, the default behaviour is to match by ROS name, but, in case of ambiguity, we allow the use of the containing package and source file, down to the line and column number, if necessary. All remaining attributes are used to replace the extracted ones. We consider it an error to provide repair hints (as opposed to creation hints) for entities that do not exist, or if there are multiple possible matches (e.g., because traceability was not specified to disambiguate). Hints always overwrite extracted attributes; they are considered to be a ground truth. As we have stated in the previous section, the runtime entities of the metamodel contain redundant information, namely Topics and Services. Thus, we limit hints to Node Instances, Parameters, and ROS Links – the essential information to build a Computation Graph. Listing 3.15 provides an example of what extraction hints for the minimal Configuration could look like in YAML syntax, if any hints were needed. In this example, we can see that a new Parameter /new_param is created (note how create is set to true ). Furthermore, the model of the /ficticontrol Node Instance is refined regarding its Publisher and Parameter Getter Links. For the former, we just refine the msg_type of a Publisher on topic /controller_cmd , by setting it to std_msgs/Float64 . For the latter, we create a new Link, connected to the Parameter we have just defined. A more complex example can be seen, for instance, in the TurtleBot2 robot, one of our case studies in Chapter 8. Subscribers are created within a loop, reading topic names from a given list of strings. The automatic extraction is unable to resolve the ROS name argument because it is a dynamic value. We can 3.3. Model Extraction 64 1configurations: 2minimal: 3# launch commands, etc. 4hints: 5nodes: 6/ficticontrol: 7publishers: 8-name:"/controller_cmd" 9type:"std_msgs/Float64" 10 getters: 11 -name:"/new_param" 12 create: true 13 type:"int" 14 traceability: 15 package:"fictibot_controller" 16 file:"src/random_controller.cpp" 17 line: 42 18 column: 3 19 parameters: 20 /new_param: 21 create: true 22 type:"int" 23 default_value: 1 24 traceability: null Listing 3.15: Example extraction hints in YAML syntax. solve this by providing one repair hint that matches this primitive call, for the first entity created in the loop, and then provide the remaining entities as create hints. Lastly, the application of extraction hints should follow a specific order: 1. application of extraction hints to Parameters; 2. application of extraction hints to Node Instances; 3. application of extraction hints to Links. This approach aims to maximise the expressive power of hints, minimise name conflicts and make them more intuitive. We start with Parameters, as these are mostly independent entities, and in a ROS environment they would be set on the Parameter Server before launching nodes. Creating Parameters first also allows specified Links to use these Resources right away; the other way around would lead to Links implicitly creating new Parameters that would have to be matched against the hints. We leave the refinement and creation of Links for last because the creation of new Node Instances is again based on a Node, and on the instantiation of ROS Primitive Calls to create the initial set of Links. The fresh Links will inherit any unresolved values from the parent Primitive Calls, which can then be resolved by applying hints. In summary, we propose a simple approach where hints are regarded as the ground truth, even though they might not describe every aspect of the model. This ground truth is used to extend the model or to refine it, entity by entity. Every part of the ground truth must be present in the final model, as mentioned. An interesting consequence of this approach is that it enables users to fully specify (the runtime entities of) a system from scratch via hints, even when the extraction process produces an empty computation 3.4. Summary 65 graph. This is useful, for instance, to overcome the limitations of an implementation, such as dealing with unsupported programming languages – e.g., supporting C ++ but not Python, and providing all Python nodes via hints. In a sense, it plays nicely with both the traditional code-first development processes, or the more formal model-driven ones. 3.4 Summary A domain-specific ROS analysis requires, in some form, a model of the target ROS system based around the core concepts of ROS, such as nodes, topics and services. Conveniently, the ROS documentation already lays out an abstraction for the system’s runtime: the ROS Computation Graph. However, the main purpose of finding defects is to correct them, and the entities of the computation graph, by themselves, do not point at the origin of those defects, in the source code. Traceability is a key ingredient that any ROS architectural model should contain. The main problem is that building such a complex model by hand, in an environment that encourages dynamic architectures, entails a considerable volume of error-prone work and volatile data. Thus, automatic model extraction (or reverse engineering) becomes more of a necessity rather than a mere convenience. In this chapter, we presented the state of the art in architectural modelling and architecture extraction, followed by a metamodel for ROS architectures and an automatic extraction procedure based on static analysis. The proposed metamodel retains traceability information and allows for a dual view of the system, from a file system perspective and from a runtime perspective, relying mostly on concepts that are already staples of ROS. This contribution, already published in [ 151 ], improves the comprehension of ROS systems and enables reasoning about their design at static time. Achieving the same, manually, through source code inspection would be infeasible for large systems under development. The proposed extraction procedure, being based on static analysis, is, in general, incomplete, although sound. We acknowledge and address this problem by introducing uncertainty points in the metamodel, as well as allowing the external specification of extraction hints in order to refine extracted models by resolving some of those uncertainties. An evaluation of the proposed extraction process is done in Chapter 8. 4 BEHAVIOURAL PROPERTY SPECIFICATION The previous chapter was dedicated to the definition of an architectural model for ROS systems and the corresponding automated extraction process from source artefacts. It is evident that the metamodel is mostly concerned with the structure of the system. In this chapter we propose a language specially tailored for the specification of behavioural properties, both for individual nodes and full applications. Depending on the intended analysis, such properties can be taken as assumptions about the system, or as verification goals. This chapter presents the syntax and semantics for this behavioural property specification language. 4.1 State of the Art Specifying system behaviour inevitably comes down to describing observable actions, outputs, and how they relate to each other (e.g., causality) or when they should manifest. There are various ways to accomplish it, but temporal logics are especially fit for this purpose. T e m p o r a l L o g i c s Temporal logics, as implied by the name, must provide an abstraction for time. Two of the most common approaches to this problem are Linear Temporal Logic (LTL) [ 140 ] and Computation Tree Logic (CTL) [ 49 ]. The former views time, and the future in particular, as pre-determined, i.e., a program execution is treated as a single trace of events, over which one encodes formulae. The latter, by contrast, is a branching-time logic, meaning that computations are structured as a tree of possible paths that a program can follow. This view is more closely related to the control flow of programs. Both LTL and CTL have been extensively used in program verification, with applications in model checking being the most prominent. As to which is the superior choice, there is no clear answer and there are arguments in favour to both sides [ 165 ]. Both have limitations in their expressiveness; some properties can be expressed with one, but not the other. The tree nature of CTL enables efficient verification algorithms that are linear in the size of the specification, as opposed to LTL which is exponential. This is one of the reasons for CTL to be the backbone of several model checkers, and for its extensive use in industry. However, some important properties, such as strong fairness, can be specified in LTL, but cannot be specified in CTL. In addition, the branching aspect of CTL, which adds a layer of complexity to the language, is rarely a necessity for most specifications. Overall, not only is LTL more intuitive, it is also amenable to semi-formal verification [ 66 ] – verification techniques that, while not exhaustive, are effective 66 4.1. State of the Art 67 at finding defects by focusing on falsification. As in [ 165 ], we argue in favour of LTL and its extensions for the specification of robotic behaviour. Standard LTL often considers only future modalities, i.e., properties are expressed in terms of the present and future time instants only. Two common examples are the  (always) and the ♦ (eventually) operators. For a formula 𝜑 , the formula 𝜑 states that 𝜑 must always hold, from the current instant onward. Similarly, the formula ♦𝜑 states that 𝜑 must hold at the current instant or at some point in the future, at least once. A common variant of LTL is the Linear Temporal Logic with past operators. This variant adds past-time modalities to the logic that allow specifications to refer to past states or events, besides the traditional future ones. For instance, the  (historically) and  (once) operators are often introduced as the past equivalents of the  and ♦ operators, respectively. Including past modalities does not make the logic any more expressive, however [ 71 ], and there are ways to convert a past-time or mixed formula to pure-future LTL [ 70 ]. The main benefits of introducing past-time operators are the syntactic reduction of some formulae (up to an exponential factor [ 117 ]) and a significant improvement regarding formulae comprehension. A common (yet simple) example to show its convenience is the property “ 𝜓 should always be preceded by 𝜑 ” . This is expressed in pure LTL using the until (𝒰) operator. ¬((¬𝜑) 𝒰 (𝜓 ∧ ¬𝜑)) The formula uses a double negative to state that “it is not true that 𝜑 never holds until the time instant when 𝜓 holds” . With past modalities enabled, this property is reduced to the much more intelligible “it is always the case that if 𝜓 holds at the current instant, 𝜑 held at least once in the past” , written as follows. (𝜓 → 𝜑) Over the remainder of this chapter we will refer to the standard, Kripke-style syntax and semantics of LTL operators, both in future and past modalities. Starting with the syntax, let Σ be a countable set of atomic propositions. Definition 1. LTL formulae over Σ are inductively defined: (i) For 𝑝 ∈ Σ , 𝑝 is a formula. (ii) For 𝜑 and 𝜓 formulae, (¬𝜑) , (𝜑 ∧ 𝜓) and (𝜑 ∨ 𝜓) are formulae. (iii) For 𝜑 and 𝜓 formulae, (e 𝜑) , (u 𝜑) , (♦𝜑) , (𝜑) , (𝜑) , (𝜑) , (𝜑𝒰𝜓) , and (𝜑𝒮𝜓) are formulae. As for the semantics, formulae are evaluated over temporal frames (ℕ,≤) – a pair of a set ( ℕ in this case) and a binary relation on that set ( ≤ ), called precedence. The precedence relation is a total order ; for 𝑎,𝑏, 𝑐 ∈ ℕ: • it is antisymmetric – if 𝑎 ≤ 𝑏 and 𝑏 ≤ 𝑎, then 𝑎 = 𝑏; • it is transitive – if 𝑎 ≤ 𝑏 and 𝑏 ≤ 𝑐, then 𝑎 ≤ 𝑐; • it is connex – it is true that 𝑎 ≤ 𝑏 or 𝑏 ≤ 𝑎. Let ℳ = (ℕ,≤,𝑣) be a temporal model, where (ℕ,≤) is a temporal frame, and 𝑣 ∶ ℕ×Σ ↦ {⊤, ⊥} is a valuation assigning a truth value to each atomic proposition 𝑝∈Σ at a given time instant 𝑖 ∈ ℕ . 4.1. State of the Art 68 The temporal model ℳ is said to satisfy a formula 𝜑 , written ℳ ⊨ 𝜑 , if and only if ℳ,0 ⊨ 𝜑 . Given an atomic proposition 𝑝 , time instants 𝑖 , 𝑗 and 𝑘 , and formulae 𝜑 and 𝜓 , the semantics of LTL operators is presented in Figure 30. ℳ,𝑖 ⊨ ⊤ ℳ,𝑖 ⊭ ⊥ ℳ,𝑖 ⊨ 𝑝 iff 𝑣(𝑖, 𝑝) ℳ,𝑖 ⊨ ¬𝜑 iff ℳ,𝑖 ⊭ 𝜑 ℳ,𝑖 ⊨ 𝜑 ∧ 𝜓 iff ℳ, 𝑖 ⊨ 𝜑 and ℳ,𝑖 ⊨ 𝜓 ℳ,𝑖 ⊨ 𝜑 ∨ 𝜓 iff ℳ, 𝑖 ⊨ 𝜑 or ℳ,𝑖 ⊨ 𝜓 ℳ,𝑖 ⊨ e 𝜑iff ℳ,𝑖 + 1 ⊨ 𝜑 ℳ,𝑖 ⊨ u 𝜑iff 𝑖 > 1 and ℳ,𝑖 − 1 ⊨ 𝜑 ℳ,𝑖 ⊨ ♦𝜑iff ℳ,𝑗 ⊨ 𝜑 for some 𝑗such that 𝑖 ≤ 𝑗 ℳ,𝑖 ⊨ 𝜑iff ℳ,𝑗 ⊨ 𝜑 for some 𝑗such that 𝑗 ≤ 𝑖 ℳ,𝑖 ⊨ 𝜑iff ℳ,𝑗 ⊨ 𝜑 for all 𝑗such that 𝑖 ≤ 𝑗 ℳ,𝑖 ⊨ 𝜑iff ℳ,𝑗 ⊨ 𝜑 for all 𝑗such that 𝑗 ≤ 𝑖 ℳ,𝑖 ⊨ 𝜑𝒰𝜓 iff ℳ, 𝑗 ⊨ 𝜓 for some 𝑗such that 𝑖 ≤ 𝑗 and ℳ,𝑘 ⊨ 𝜑 for every 𝑘such that 𝑖 ≤ 𝑘 < 𝑗 ℳ,𝑖 ⊨ 𝜑𝒮𝜓 iff ℳ, 𝑗 ⊨ 𝜓 for some 𝑗such that 𝑗 ≤ 𝑖 and ℳ,𝑘 ⊨ 𝜑 for every 𝑘such that 𝑗 < 𝑘 ≤ 𝑖 Figure 30: Semantics of LTL operators. S p e c i f i c a t i o n B a s e d o n L T L Linear Temporal Logic has been used extensively for property specification with applications in model checking [ 17 , 50 , 83 , 104 ], runtime verification [ 21 , 23 , 32 , 106 , 126 ] or testing [ 125 , 138 , 161 ]. But, even though LTL is considered to be more intuitive than CTL, specification mistakes are bound to happen at some point. To overcome this threat, and, in a way, to lower the barrier to adoption of automated verification, Dwyer et al. proposed a catalogue of patterns for specification problems [58,59] as follows. 1. Absence: 𝜑is always false. 2. Universality: 𝜑is always true. 3. Existence: 𝜑is true at least once. 4. Bounded Existence: 𝜑is true at most 𝑛times. 5. Precedence: 𝜑is a necessary precondition for 𝜓. 6. Response: 𝜑must be followed by an occurrence of 𝜓. 7. Precedence Chain: Generalisation of Precedence to 𝑚causes and 𝑛effects. 8. Response Chain: Generalisation of Response to 𝑚stimuli and 𝑛responses. Such patterns were put together based on experience, and represent properties that are often desirable or required in various concurrent or reactive systems. Each pattern can be further refined with a scope , limiting the extent to which the property must hold. The scope can be global (the entire execution), before 𝜑 (the whole execution up to 𝜑 ), after 𝜑 (the whole execution starting from 𝜑 ), between 𝜑 and 𝜓 (where 4.1. State of the Art 69 both events must occur), or after 𝜑until 𝜓 (similar to between , but 𝜓 is not required to occur, in which case the property must hold forever after the last occurrence of 𝜑 ). Mappings of these patterns to LTL, CTL and other logics have been proposed1[58,59], facilitating their adoption. Bauer and Leucker expand the idea of specification patterns further with SALT [ 22 ], a specification and assertion language that incorporates the previous patterns and extends them with notions of real time, exceptions to normal behaviour and regular expressions. In terms of expressiveness, the untimed fragment of SALT is as expressive as LTL, while its timed fragment is as expressive as Timed LTL, a temporal logic based on automata with clocks (also known as state-clock logic [ 56 , 146 ]). Another improvement over Dwyer et al.’s patterns is the generalisation of scopes. In SALT, scopes can be nested, adding a layer of complexity in exchange for increased flexibility and specificity of the specifications. E x t e n s i o n s t o L i n e a r T e m p o r a l L o g i c Two major limitations of LTL for the purposes of specifications are its inability to express properties in terms of real time, and its lack of first-order predicates. Metric Temporal Logic (MTL [ 97 ]) addresses the former, and First-Order Temporal Logic (FOTL [ 116 ]) was proposed to address the latter. Despite being useful extensions on their own, especially when including past-time modalities, complex systems (such as robots) inevitably require the full set of features. Metric First-Order Temporal Logic (MFOTL [ 46 ]) is a logic that incorporates the benefits of both MTL and FOTL. Given its relevance for the specification language presented in this chapter, herein we present the syntax and semantics of MFOTL. M e t r i c F i r s t - O r d e r T e m p o r a l L o g i c Temporal operators in MFOTL can be annotated with (metric time) intervals. A temporal formula is only satisfied if it is satisfied within the bounds given by the time interval of the temporal operator, which is always relative to a time stamp. Let Δ be the set of non-empty intervals over ℕ0 . We write an interval 𝛿 ∈ Δ as [𝛿1,𝛿2) , where 𝛿1∈ ℕ0 , 𝛿2∈ ℕ ∪ {∞} , and 𝛿1< 𝛿2 , i.e., [𝛿1,𝛿2) ∶= {𝑡 ∈ ℕ0∶ 𝛿1≤ 𝑡 < 𝛿2} . A signature 𝑆 is a tuple ( C , P ,𝑎) , where Cis a finite set of constant symbols, Pis a finite set of predicates disjoint from C, and the function 𝑎 ∶ P ↦ ℕ provides the arity 𝑎(𝑝) ∈ ℕ of each predicate 𝑝 ∈ P. Also, let Vdenote a countably infinite set of variables, where we assume that V∩ (C∪P) = ∅, for all signatures. Definition 2. The formulae over 𝑆 are inductively defined: (i) For 𝑥, 𝑦 ∈ V ∪ C , 𝑥 = 𝑦 is a formula. (ii) For 𝑝 ∈ P , 𝑛 = 𝑎(𝑝) and 𝑥1,… ,𝑥𝑛∈ V ∪ C , 𝑝(𝑥1,… ,𝑥𝑛) is a formula. (iii) For 𝑥 ∈ V , if 𝜑 and 𝜓 are formulae, then (¬𝜑) , (𝜑 ∧ 𝜓) and (∃𝑥 ∶ 𝜑) are formulae. (iv) For 𝛿 ∈ Δ , if 𝜑 and 𝜓 are formulae, then (u 𝛿𝜑) , (e 𝛿𝜑) , (𝜑𝒮𝛿𝜓) , and (𝜑𝒰𝛿𝜓) are formulae. We provide only the syntax and semantics for a core set of MFOTL operators (Figure 31). Other common operators can be defined in terms of the core set, as shown in Figure 32. To fully define the semantics of MFOTL, a few additional notions are required. A first-order structure 𝐷 over 𝑆 consists of a domain |𝐷| ≠ ∅ and interpretations 𝑐𝐷∈ |𝐷| and 𝑝𝐷⊆ |𝐷|𝑎(𝑝) , for each 𝑐 ∈ Cand 𝑝 ∈ P. A temporal 1https://matthewbdwyer.github.io/psp/patterns.html 4.3. Language Syntax 76 of operators, we can assume a number of syntactic sugar operators, such as the relational operator ‘>’ or the division operator ‘/’. With the forall quantifier, we provide a basic means of iterating over array fields. This is intended to iterate over all valid indices of the array, rather than the values directly. For instance, the syntax ‘forall i in array’ is roughly equivalent to the Python for iin range(len(array)). The grammar also captures references to quantified variables ( ‘$var’ ), and to message fields (either of the message associated to the event, or to other messages with the ‘@’ symbol). Message fields can be simple identifiers to refer directly to a field of the current message ( ‘field’ ), multiple identifiers separated by dots to refer to nested fields of composed messages ( ‘parent.child’ ), or indexed to access array positions ( ‘parent.array[1]’ ). Regarding cross-references to other messages, every message has an implicit associated index to be used with ‘@’ . Messages are numbered, starting at 1 with the activator event, and then with 2 for the first pattern event. Other events are not referenced in the current version of the language. Since numeric references can become confusing, we introduce event aliases , a syntactic sugar layer that replaces numeric references to other messages with human-readable names instead. For instance, an activator event ‘ /bumper as Bumper ’ would allow predicates to refer to this message as ‘@Bumper’ rather than ‘@1’ . Message fields would be accessed as ‘@Bumper.field’ , for instance. We reiterate that this is just a syntactic replacement, and thus has no effect over the language’s semantics. We also note that not all events can refer to each other arbitrarily, for temporal and semantic reasons; an event can only refer to another event that, unambiguously, happened before it. For example, activator and terminator events must be independent, but pattern events can refer to the scope activator. The semantic limitations that require independent terminator events are explained in Section 4.4. 4.3.4 Examples This subsection provides some syntax examples for Fictibot properties. We start off with an example of the Absence pattern with a global scope. Consider the following property for the Fictibot Driver. At all times, all data published on /bumper is within the range [0,7]. The property has to be encoded in the negative form; stating that only the values between 0 and 7 are allowed is the same as stating that no other value is allowed. As such, the property becomes: 1globally:no /bumper {data < 0 or data > 7} Examples of the Existence pattern assert that a certain message shall be published. We can use it, for instance, to specify some properties of system initialisation. Within the first 500 milliseconds after launching, a message shall be published on /bumper . This property does not impose any restriction on the message itself, thus it contains no predicates, but it does use the timed variant of the pattern. 4.4. Language Semantics 77 1globally:some /bumper within 500 ms The Fictibot Multiplexer is, in essence a state machine. It provides the ideal setting to use the After-Until scope, to model the node’s states. Combined with the Precedence pattern, we can assert properties such as the following. While in a high priority state (messages on /state carry data > 0 ), publishing a message on /controller_cmd is preceded by receiving an exactly equal message on /high_priority_cmd, in the preceding 100 milliseconds. 1after /state {data > 0} until /state {not data > 0}: /controller_cmd as CMD 2requires /high_priority_cmd {data = @CMD.data} within 100 ms The Response pattern, conversely to the Precedence pattern, specifies an event that should happen after the stimulus event. It is adequate to specify reactive systems, such as safety controllers and some aspects of the Fictibot Random Controller. At all times, receiving a /bumper message such that data ≠ 0 leads to the publication of a message on /normal_priority_stop, within, at most, 200 milliseconds. The syntax for this property is as follows: 1globally:/bumper {not data = 0} causes /normal_priority_stop within 200 ms Lastly, an example of the Prevention pattern in this system would be the time-based nature of the Fictibot Multiplexer’s states. After entering a high priority state, the Multiplexer should remain in that state for, at least, 1 second. 1globally:/state {data > 0} forbids /state {not data > 0} within 1000 ms 4.4 Language Semantics We define the semantics of our specification language in terms of the semantics of MFOTL. That is, given a syntactic construct of the language Φ , we define its interpretation as the equivalent MFOTL formula and denote it as JΦK. We require only a few additional definitions beforehand. Let 𝕄 be the set of all messages , where a message consists of a unique identifier. The first-order structures 𝐷𝑖over 𝑆consist of a domain |𝐷| such that •|𝐷| contains all numbers, i.e., ℝ ⊂ |𝐷|; •|𝐷| contains all Boolean values, i.e., {⊤,⊥} ⊂ |𝐷|; •|𝐷| contains all strings, i.e., 𝕊 ⊂ |𝐷|, with 𝕊the set of all strings; 4.4. Language Semantics 78 •|𝐷| contains all messages, i.e., 𝕄 ⊂ |𝐷|. Let 𝕋 be the set of all ROS topics. For all /t ∈ 𝕋 we define a predicate 𝑡 ∈ Psuch that 𝑡(𝑚) is true if and only if a message 𝑚 ∈ 𝕄 can be observed on topic /t . The relation of messages to data fields is given by predicates field (𝑚,𝑥) ∈ Psuch that, for a message 𝑚 , field (𝑚,𝑥) holds if and only if 𝑚 carries the value (or message) 𝑥in a data field named field. Array fields are only slightly different. To simplify quantification over the indices of an array, we redefine the usual predicate field (𝑚,𝑘) , to hold for all indices belonging to the array, rather than values. That is, for 𝑘 ∈ ℕ0 , field (𝑚,𝑘) holds if 𝑘 is an index of an array named field . In addition, we define a predicate field 𝑘(𝑚,𝑥) for all indices 𝑘 , such that field 𝑘(𝑚,𝑥) holds if the field field[k] carries the value 𝑥 , i.e., if field (𝑚,𝑘) holds and the array contains 𝑥at the index 𝑘. We address composed messages with predicate composition. That is, for a data field f.g , we use the composition of predicates 𝑓and 𝑔, such that 𝑔 ∘ 𝑓(𝑚,𝑥) ≡ (∃𝑚′∶ 𝑓 (𝑚,𝑚′) ∧ 𝑔(𝑚′,𝑥)) To shorten some formulae, and to improve readability, we assume that all interpreted properties Φ are type-checked prior to their semantic interpretation JΦK . For instance, in the case of arithmetic operators, for an expression 𝑎+𝑏 , we assume that both 𝑎 and 𝑏 are such that 𝑎,𝑏 ∈ ℝ . Otherwise, we would have to introduce a new predicate, 𝑖𝑠𝑁𝑢𝑚𝑏𝑒𝑟(𝑥) , such that for all 𝑥 , 𝑖𝑠𝑁𝑢𝑚𝑏𝑒𝑟(𝑥) holds if 𝑥 ∈ ℝ , and replace every arithmethic-related formula 𝜑with 𝑖𝑠𝑁𝑢𝑚𝑏𝑒𝑟(𝑎) ∧ 𝑖𝑠𝑁𝑢𝑚𝑏𝑒𝑟(𝑏) ∧ 𝜑. Definition 4. Let (𝐷,𝜏) be a temporal structure over 𝑆 , with 𝐷 = (𝐷0,𝐷1, …) and 𝜏 = (𝜏0, 𝜏1,…) . Let 𝑣 be a valuation, 𝑖 ∈ ℕ0 and Φ a property over 𝑆 . We define JΦK , the interpretation of Φ , as a function that translates Φ to its equivalent Metric First-Order Temporal Logic formula. Thus, we define (𝐷,𝜏, 𝑣,𝑖) ⊨ Φ as (𝐷,𝜏, 𝑣, 𝑖) ⊨ JΦK , and JΦK is defined as follows. Scopes Jglobally:ΨK≜JΨK∅ ⊥ Jafter 𝑝:ΨK≜(∀𝑥 ∶ enterScope (𝑝,⊥, 𝑥) → JΨK𝑥 ⊥) Juntil 𝑞:ΨK≜JΨK∅ 𝑞 Jafter 𝑝until 𝑞:ΨK≜(∀𝑥 ∶ enterScope (𝑝,𝑞, 𝑥) → JΨK𝑥 𝑞) enterScope (𝑝,𝑞, 𝑥) ≜J𝑝K𝑥∧ ¬(∃𝑦 ∶ J𝑞K𝑦) ∧ 𝒵(¬(∃𝑦 ∶ J𝑝K𝑦) ℬ (∃𝑦 ∶ J𝑞K𝑦)) In the presented translation semantics we can see the use an auxiliary predicate, enterScope , that deserves further explanation. The globally and until scopes start, by definition, at the initial instant of the trace and, thus, require the resulting formula to be true when evaluated at that instant. On the other hand, the after and after-until scopes do not start until the matching event has been observed. We 4.4. Language Semantics 79 know that a property must only hold within its scope, so the resulting formulae have to account for this when evaluated at the initial instant of the trace – recall that a temporal structure (𝐷,𝜏) satisfies a formula 𝜑 , written (𝐷,𝜏) ⊨ 𝜑 , if and only if (𝐷,𝜏, 𝑣, 0) ⊨ 𝜑 , for a valuation 𝑣 . In addition, the after-until scope is (possibly) reentrant, which means that the activation of a scope might be observed multiple times. This is why these two scopes require the  operator – so that, whenever an event marks the start of the scope of a property, we can evaluate the inner pattern. Hence, given activator and terminator events 𝑝 and 𝑞 , and given a message 𝑥 , enterScope (𝑝,𝑞, 𝑥) holds if and only if the message 𝑥 starts the scope at the current instant. More precisely, enterScope (𝑝,𝑞, 𝑥) holds if its three conjuncts are satisfied: •𝑥matches the event 𝑝, i.e., 𝑥is an activator message; and • no message at that instant matches 𝑞(as it would terminate the scope immediately); and • in the previous instants, since either the initial instant or the last terminator event (for reentrant scopes), there has been no other activator, i.e., 𝑥 is the first match for 𝑝 (further matches when within the scope are ignored). The third conjunct of enterScope imposes a limitation on the language. Due to its reference to a previous scope, and due to the semantics of MFOTL, terminator events must be independent; a terminator event cannot reference previous events (i.e., the scope activator). If such cross-references were allowed, we would need to pass additional messages in the superscript vector of J𝑞K𝑦 , such as J𝑞K𝑥,𝑦 . But, in the third conjunct, the back-to operator refers to the terminator of a previous scope (which would also have references), and we cannot say, at that instant, which message opened the scope of that terminator. In summary, allowing terminator events to refer to activator events would make the definition of enterScope recursive. Note that, for the translation of patterns and predicates, we used superscript and subscript annotations. This is mostly a convenience to present the translation in a compositional fashion, from a top-down perspective, and to allow us to carry over to the lower levels of the translation some variables that were introduced at the higher levels. For instance, in JΨK𝑥 𝑞 , the superscript 𝑥 is a vector of quantified messages. In the translation of after and after-until , this vector contains a single message, the scope activator message. In the translation of globally and until , it is ∅ , representing an empty vector. Similarly, the superscript ∅ represents a vector containing zero messages. The subscript 𝑞 is used to carry over the terminator event from the scope to the translation of the pattern. The same notation applies to J𝑝K𝑥 , except that 𝑝is a predicate, rather than a pattern. 4.4. Language Semantics 80 Patterns Jno 𝑏K𝑥 𝑞≜ ¬(∃𝑦 ∶ J𝑏K𝑥,𝑦) 𝒲 (∃𝑦 ∶ J𝑞K𝑦) Jno 𝑏within 𝛿msK𝑥 𝑞≜ ¬(∃𝑦 ∶ J𝑏K𝑥,𝑦) 𝒲[0,𝛿) (∃𝑦 ∶ J𝑞K𝑦) Jsome 𝑏K𝑥 𝑞≜ ¬(∃𝑦 ∶ J𝑞K𝑦) 𝒰 ((∃𝑦 ∶ J𝑏K𝑥,𝑦) ∧ ¬(∃𝑦 ∶ J𝑞K𝑦)) Jsome 𝑏within 𝛿msK𝑥 𝑞≜ ¬(∃𝑦 ∶ J𝑞K𝑦) 𝒰[0,𝛿) ((∃𝑦 ∶ J𝑏K𝑥,𝑦) ∧ ¬(∃𝑦 ∶ J𝑞K𝑦)) J𝑎causes 𝑏K𝑥 𝑞≜ (∀𝑦 ∶ J𝑎K𝑥,𝑦 →Jsome 𝑏K𝑥,𝑦 𝑞) 𝒲 (∃𝑦 ∶ J𝑞K𝑦) J𝑎causes 𝑏within 𝛿msK𝑥 𝑞≜ (∀𝑦 ∶ J𝑎K𝑥,𝑦 →Jsome 𝑏within 𝛿msK𝑥,𝑦 𝑞) 𝒲 (∃𝑦 ∶ J𝑞K𝑦) J𝑎forbids 𝑏K𝑥 𝑞≜ (∀𝑦 ∶ J𝑎K𝑥,𝑦 →Jno 𝑏K𝑥,𝑦 𝑞) 𝒲 (∃𝑦 ∶ J𝑞K𝑦) J𝑎forbids 𝑏within 𝛿msK𝑥 𝑞≜ (∀𝑦 ∶ J𝑎K𝑥,𝑦 →Jno 𝑏within 𝛿msK𝑥,𝑦 𝑞) 𝒲 (∃𝑦 ∶ J𝑞K𝑦) J𝑏requires 𝑎K𝑥 𝑞≜ ∀𝑦 ∶ prec (𝑎,𝑏, 𝑞,𝑥, 𝑦) J𝑏requires 𝑎within 𝛿msK𝑥 𝑞≜ ∀𝑦 ∶ prec (𝑎,𝑏, 𝑞,𝑥, 𝑦) ∧ once 𝛿(𝑎,𝑏, 𝑞,𝑥, 𝑦) prec (𝑎,𝑏, 𝑞,𝑥, 𝑦) ≜ ¬J𝑏K𝑥,𝑦 𝒲 (∃𝑧 ∶ J𝑎K𝑥,𝑦,𝑧 ∨J𝑞K𝑧) once 𝛿(𝑎,𝑏, 𝑞,𝑥, 𝑦) ≜ (J𝑏K𝑥,𝑦 →[0,𝛿)(∃𝑧 ∶ J𝑎K𝑥,𝑦,𝑧)) 𝒲 (∃𝑧 ∶ J𝑞K𝑧) For the translation of patterns, we now see additional superscript annotations, not discussed for scopes. For instance, in Jno 𝑏K𝑥 𝑞 , the superscript 𝑥 is a vector (of arbitrary length) of quantified messages that causally precede 𝑏 ; such as the activator message, or no messages at all if the vector is of zero-length. Alternatively, as we will see in following translations, we can also use the notation J𝑏K𝑥1,…,𝑥𝑛 to refer to a vector of length 𝑛 . Furthermore, the use of the superscript J𝑏K𝑥,𝑦 means that the translation of the predicate 𝑏should consider a vector of all messages in 𝑥plus the quantified message 𝑦. We can see that the unary patterns, no and some have a translation that is already close a MFOTL formula, save for the translation of the event predicates, J𝑏K and J𝑞K . The binary patterns causes and forbids are translated via composition, reusing the translations of the previous unary patterns. The last binary pattern, requires , is more complex, and is defined with the use of auxiliary predicates for readability purposes. The first of these predicates, prec (𝑎,𝑏, 𝑞,𝑥, 𝑦) states that the event 𝑏 (the behaviour) should not happen before 𝑎 (the required event) or 𝑞 (the scope terminator). When adding real-time constraints, however, we also need the predicate once 𝛿(𝑎,𝑏, 𝑞,𝑥, 𝑦) , which states that, if the event 𝑏 happens before the scope terminator, then the required event 𝑎 must have happened within the specified interval (the previous 𝛿 time instants). The remaining translations, J𝑎K , J𝑏K and J𝑞K all represent predicate translations, which we present next. 4.4. Language Semantics 81 Predicates J⊤K𝑥≜ ⊤ J⊥K𝑥≜ ⊥ J/topic K𝑥1,…,𝑥𝑛≜ topic (𝑥𝑛) J/topic {𝜑}K𝑥1,…,𝑥𝑛≜ topic (𝑥𝑛) ∧ J𝜑K𝑥1,…,𝑥𝑛 ∅ J(𝜑)K𝑥 𝛾≜ (J𝜑K𝑥 𝛾) Jnot 𝜑K𝑥 𝛾≜ ¬J𝜑K𝑥 𝛾 J𝜑and 𝜓K𝑥 𝛾≜J𝜑K𝑥 𝛾∧J𝜓K𝑥 𝛾 J𝜑or 𝜓K𝑥 𝛾≜J𝜑K𝑥 𝛾∨J𝜓K𝑥 𝛾 Jforall var in 𝑓:𝜑K𝑥 𝛾≜ ∀𝑦 ∶ 𝑦 J𝑓K𝑥 𝛾→J𝜑K𝑥 𝛾[var↦𝑦] Jforall var in @𝑘.𝑓:𝜑K𝑥 𝛾≜ ∀𝑦 ∶ 𝑦 J@𝑘.𝑓K𝑥 𝛾→J𝜑K𝑥 𝛾[var↦𝑦] J𝑎 = 𝑏K𝑥 𝛾≜ ∃𝑦,𝑧 ∶ 𝑦 J𝑎K𝑥 𝛾∧𝑧 J𝑏K𝑥 𝛾∧ 𝑦 = 𝑧 J𝑎 < 𝑏K𝑥 𝛾≜ ∃𝑦,𝑧 ∶ 𝑦 J𝑎K𝑥 𝛾∧𝑧 J𝑏K𝑥 𝛾∧ 𝑦 < 𝑧 The translations of most predicates are relatively straightforward. Atomic predicates, such as ⊤ and ⊥ are directly translated. Top-level predicates, including a topic name, translate to a predicate with the same name as the topic, as previously explained, that checks whether the last message of the superscript vector is present in that topic, at the given time instant (i.e., the message can be observed at that time). Simple logic operators, not , and , or , translate to their respective logic operators and propagate the translation of subformulae. Quantifiers and atomic formulae are not as intuitive. In this semantics, most expressions are singleton values; the exception lies in array message fields, that can represent multiple values. Namely, the predicate with the name of the array field denotes every index of the array. In contrast, for simple message fields we use field (𝑥, 𝑦) to denote a predicate that tests whether 𝑦 is a value of the homonymous field in message 𝑥 . Thus, when translating expressions in general, we use the notation 𝑦 J𝑎K𝑥 𝛾 to represent a predicate that tests whether the value of the variable 𝑦 is one of the possible values for the expression 𝑎. To handle new variable definitions for quantification, we use an additional 𝛾 subscript. This subscript is a mapping of syntactic replacements; given a variable name as written in the property , we can replace its occurrences with a quantified variable in |𝐷| . For instance, given the predicate ‘ forall iin array: array[$i] = 0 ’, we quantify over all values for which 𝑦 JarrayK𝑥 𝛾 holds, i.e., all the indices of the array, as we will see next. For such values, 𝑦 , the result of Jarray[$i] = 0 K𝑥 𝛾[i↦𝑦] must hold. This is equivalent to stating that, in the translation of array[$i] = 0 we should replace every occurrence of $i with the quantified variable 𝑦(the array index). Atomic formulae, such as 𝑎 = 𝑏 , would, intuitively, just translate the left and right operands, as in J𝑎K𝑥 𝛾=J𝑏K𝑥 𝛾 . This, however, is not possible, due to expressions having multiple possible values (in 4.4. Language Semantics 82 general), as previously explained. We require existential quantification to bind variables to their respective values. Then, the = and < operators can only be applied to expressions that denote singleton values. The use of array fields, an expression that does not represent a singleton value, is confined to quantification. Values and Expressions 𝑦 J(𝑎)K𝑥 𝛾≜ (𝑦 J𝑎K𝑥 𝛾) 𝑦 J-𝑎K𝑥 𝛾≜ ∃𝑧 ∶ 𝑧 J𝑎K𝑥 𝛾∧ 𝑦 = −𝑧 𝑦 J𝑎+𝑏K𝑥 𝛾≜ ∃𝑧, 𝑤 ∶ 𝑧 J𝑎K𝑥 𝛾∧𝑤 J𝑏K𝑥 𝛾∧ 𝑦 = (𝑧 + 𝑤) 𝑦 J𝑎*𝑏K𝑥 𝛾≜ ∃𝑧, 𝑤 ∶ 𝑧 J𝑎K𝑥 𝛾∧𝑤 J𝑏K𝑥 𝛾∧ 𝑦 = (𝑧 × 𝑤) 𝑦 J𝑐K𝑥 𝛾≜ 𝑦 = 𝑐 𝑦 J$varK𝑥 𝛾≜ 𝑦 = 𝛾(var) 𝑦 J𝑓K𝑥1,…,𝑥𝑛 𝛾≜J𝑓K𝛾(𝑥𝑛,𝑦) 𝑦 J@𝑘.𝑓K𝑥1,…,𝑥𝑛 𝛾≜J𝑓K𝛾(𝑥𝑘,𝑦) if 1 ≤ 𝑘 ≤ 𝑛 JfieldK𝛾≜ field Jfield[𝑘]K𝛾≜ field 𝑘 Jfield[$var]K𝛾≜ field 𝛾(var) J𝑓1.𝑓2K𝛾≜J𝑓2K𝛾∘J𝑓1K𝛾 The translations of values and expressions are the last step to obtain a MFOTL formula. There is nothing new at this point, except field references to other messages, e.g., @𝑘.𝑓 . Recall that event aliases are syntactic sugar that is converted to a message index at this point, i.e., 𝑘 is a number, rather than a human-readable name. The translation for this case, then, refers to the 𝑘 -th message given in the superscript vector, 𝑥𝑘 , rather than the current message, 𝑥𝑛 . The fields themselves are translated to their homonymous predicates, and field composition translates to predicate composition, as previously explained. Arithmetic expressions are similar to the translations of atomic formulae, and 𝑐 denotes a constant symbol, such as an integer. 4.4.1 Examples We provide examples of the language’s property interpretation semantics, JΦK , using concrete traces of the Fictibot system. Consider the trace in Figure 34, for instance. Each circle in the diagram represents an event where the underlined text above or below it is the time stamp of the event and the dashed box contains the associated topic name and message data (between braces, e.g., {data: 0}). The arrows in the diagram represent the order between events in the trace, starting from the earliest event to the latest. 4.4. Language Semantics 83 Figure 34: Example trace of the Fictibot system. With slight modifications of the trace in Figure 34 we can illustrate examples of violated properties in Fictibot. The altered trace diagrams highlight the events causing the violation, using filled circles and red text for the time stamp (if it is a timing violation) or for the event’s data (if it is a predicate violation). A b s e n c e Figure 35 shows a trace excerpt where the following Absence property of the Fictibot Driver is violated. 1globally:no /bumper {data < 0 or (not data < 8)} A message is published on /bumper with a value of 8, but it is only expected to publish data between 0 and 7 (inclusive). Figure 35: Example trace of the Fictibot system violating an Absence property. We translate the property into the following formula, while also applying some simplifications to make it more readable. 4.4. Language Semantics 84 Jglobally:no /bumper {data < 0 or (not data < 8)}K iff Jno /bumper {data < 0 or (not data < 8)}K∅ ⊥ iff ¬(∃𝑥 ∶ J/bumper {data < 0 or (not data < 8)}K𝑥) 𝒲 (∃𝑥 ∶ J⊥K𝑥) iff ¬(∃𝑥 ∶ J/bumper {data < 0 or (not data < 8)}K𝑥)𝒲⊥ iff (¬(∃𝑥 ∶ J/bumper {data < 0 or (not data < 8)}K𝑥)) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ Jdata < 0 or (not data < 8)K𝑥 ∅)) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ (Jdata < 0K𝑥 ∅∨Jnot data < 8K𝑥 ∅))) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ (Jdata < 0K𝑥 ∅∨ ¬Jdata < 8K𝑥 ∅))) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ ((∃𝑦,𝑧 ∶ 𝑦 JdataK𝑥 ∅∧𝑧 J0K𝑥 ∅∧ 𝑦 < 𝑧) ∨ ¬(∃𝑦,𝑧 ∶ 𝑦 JdataK𝑥 ∅∧𝑧 J8K𝑥 ∅∧ 𝑦 < 𝑧)))) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ ((∃𝑦,𝑧 ∶ data (𝑥, 𝑦) ∧ 𝑧 = 0 ∧ 𝑦 < 𝑧) ∨ ¬(∃𝑦,𝑧 ∶ data (𝑥, 𝑦) ∧ 𝑧 = 8 ∧ 𝑦 < 𝑧)))) iff (¬(∃𝑥 ∶ bumper (𝑥) ∧ ((∃𝑦 ∶ data (𝑥, 𝑦) ∧ 𝑦 < 0) ∨ ¬(∃𝑦 ∶ data (𝑥, 𝑦) ∧ 𝑦 < 8)))) It is easy to see that when evaluated at the initial instant of the trace, this formula does not hold. The second message of the trace, with the highlights, is a message fitting for the quantified variable 𝑥 . In particular, it is a message such that bumper (𝑥) , and one such that ¬(∃𝑦 ∶ data (𝑥, 𝑦) ∧ 𝑦 < 8) . Such conditions should never hold, as given by (¬𝜑), resulting in a violation. R e s p o n s e Figure 36 shows a trace excerpt where the following Response property of the Fictibot Random Controller is violated. 1globally:/bumper {not data = 0} causes /normal_priority_stop within 200 ms In this case, it is a violation of the timing aspect of the property. The stimulus, a /bumper message such that data ≠ 0 , should have led to the publication of a message on /normal_priority_stop . While the system does send the message, it does not respect the 200 millisecond response window. Figure 36: Example trace of the Fictibot system violating a Response property. 4.4. Language Semantics 85 We translate the property into the following formula. Jglobally:/bumper {not data = 0} causes /normal_priority_stop within 200 msK iff J/bumper {not data = 0} causes /normal_priority_stop within 200 msK∅ ⊥ iff (∀𝑥 ∶ J/bumper {not data = 0}K𝑥→Jsome /normal_priority_stop within 200 msK𝑥 ⊥) 𝒲 (∃𝑥 ∶ J⊥K𝑥) iff (∀𝑥 ∶ J/bumper {not data = 0}K𝑥→Jsome /normal_priority_stop within 200 msK𝑥 ⊥)𝒲⊥ iff (∀𝑥 ∶ J/bumper {not data = 0}K𝑥→Jsome /normal_priority_stop within 200 msK𝑥 ⊥) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬(∃𝑦 ∶ data (𝑥, 𝑦) ∧ 𝑦 = 0)) →Jsome /normal_priority_stop within 200 msK𝑥 ⊥) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬ data (𝑥, 0)) → Jsome /normal_priority_stop within 200 msK𝑥 ⊥) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬ data (𝑥, 0)) → (¬(∃𝑦 ∶ J⊥K𝑦) 𝒰[0,200) ((∃𝑦 ∶ J/normal_priority_stopK𝑥,𝑦) ∧ ¬(∃𝑦 ∶ J⊥K𝑦)))) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬ data (𝑥, 0)) → (¬⊥ 𝒰[0,200) ((∃𝑦 ∶ J/normal_priority_stopK𝑥,𝑦) ∧ ¬⊥))) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬ data (𝑥, 0)) → ♦[0,200)(∃𝑦 ∶ J/normal_priority_stopK𝑥,𝑦)) iff (∀𝑥 ∶ ( bumper (𝑥) ∧ ¬ data (𝑥, 0)) → ♦[0,200)(∃𝑦 ∶ normal _ priority _ stop (𝑦))) As per the formula above, whenever a /bumper message such that data ≠ 0 is observed, a /normal_priority_stop message (any message) must be published at most 200 milliseconds afterwards. We know from Figure 36 that such a response message exists, but not within the time window, thus falsifying the property. A f t e r - U n t i l S c o p e For illustrative purposes, we also show the translation the following Fictibot Multiplexer property. 1after /state {data > 0} until /state {not data > 0}: /controller_cmd as CMD 2requires /high_priority_cmd {data = @CMD.data} within 100 ms This is a more complex example, using both the after-until scope and a Precedence pattern. Thus, we skip the intermediate steps of the translation. 5.1. High-Assurance ROS 92 1"source": { 2"packages":4,(the project contains 4 packages in total) 3"files":37,(there are 37 Source Files within these packages) 4"languages": { 5"cpp":0.559461480,(55.95% of all code is C++) 6"python":0 7}, 8"scripts":0 9}, 10 "history": { 11 "issues": [143,202,208], (number of issues in the 3 previous runs) 12 "metrics": [9,12,12], (number of previously registered metrics) 13 "lines_of_code": [838,1297,1337], 14 "timestamps": [ 15 "2018-02-24-18-31", 16 "2018-02-28-20-46", 17 "2018-03-08-18-12" 18 ] 19 (other entries were omitted) 20 }, 21 "issues": { 22 "total":208,(there are 208 issues reported by plug-ins in total) 23 "metrics":12,(12 of these issues are related to metrics) 24 "coding":200,(200 issues are related to coding standards) 25 "ratio":"0.16",(number of issues per line of code) 26 "other":0(other types of issues) 27 } Listing 5.3: Excerpt of a JSON data file exported by HAROS. The HAROS Visualiser, as previously mentioned, produces an interactive report, based on the exported JSON data files, that users can explore. It defaults to a dashboard page (see Figure 38 for a screen capture of the most recent version of the dashboard), where the summary data is provided for a selected project. Projects can be switched on this page to load a different data set. This page sorts the information in three panels: source code statistics (e.g., number of packages and files, or the number of custom message types), analysis statistics (e.g., total number of issues reported by plug-ins) and history of several metrics. Another page includes a package overview, where packages are drawn in a graph along with the dependencies between them, and a few panels contain general package information (mostly extracted from the XML package manifests). Yet another page is dedicated to the issues reported by plug-ins – the main item of interest in the report as a whole. This page is shown in Figure 39. Issues are organised by package and can be filtered using a menu. Each issue contains the violated rule, a location in the source code (where the issue was detected), additional free text comments provided by the analysis tools, and a set of tags . HAROS provides a short, central catalogue of common rules that plug-ins can reference. New rules can be added by the plug-ins themselves, in a plug-in manifest file, as we will see. Tags are associated to rules, and serve no special purpose other than helping to categorise the issues. They are created on an ad hoc fashion, i.e., there is no central catalogue of tags. Regardless, they are the main mechanism used for filtering issues – i.e., the Filter menu can be used to only show issues containing a number of tags, or to ignore issues containing such tags. 5.1. High-Assurance ROS 93 Figure 38: Summary page of the HAROS Visualiser. Figure 39: Issue listing with the HAROS Visualiser. 5.1.2 HAROS Plug-ins Creating a plug-in for HAROS is relatively straightforward. Simply put, a plug-in is a Python package containing at least two files: plugin.yaml and plugin.py . The former is a manifest file containing metadata about the plug-in, such as its name, version, and (optionally) which programming languages does it support, as well as which metrics and rules does it analyse. New rule definitions are provided in this manifest file. As an example, consider Listing 5.4, which contains an excerpt of the manifest of one of the existing plug-ins for HAROS – a plug-in for the Radon 2 tool, a tool to gather metrics from Python source code. Most of the metadata in this file serves no special purpose other than pure information, but declaring any supported languages (Python, in this case), means that, for a file by file analysis, HAROS will only supply the plug-in with Python files. By declaring only Python support, the plug-in should never be called for analysis of C++ files, for instance. The plugin.py file is a Python script that HAROS uses to look for the plug-in’s entry points. From a top-down perspective, this is the main script of the plug-in’s implementation. The only requirements 2https://pypi.org/project/radon/ 5.1. High-Assurance ROS 94 1name: haros_plugin_radon 2version:0.1 3languages: 4python 5supported_rules:(some entries were omitted) 6max_file_length_400 7min_comment_ratio_20 8mi_below_65 9max_cyclomatic_complexity_10 10 supported_metrics:(some entries were omitted) 11 - comment_ratio 12 - cyclomatic_complexity 13 - maintainability_index 14 - sloc Listing 5.4: Plug-in manifest file in YAML syntax. imposed on this file is that it must contain at least one of the entry point functions defined by HAROS in order to be executed. Listing 5.5 shows an excerpt of this script for the Radon plug-in. We can see how it implements the file_analysis function, which is the entry point for file by file analysis used by HAROS. This is where the execution of the plug-in starts. From that point on, the plug-in can organise itself in any number of additional functions or modules. In this case, the plug-in is self-contained, with only a few helper functions that call the various metrics measurement functions of the underlying tool. Throughout the code, we can see how the plug-in reports metrics and threshold violations to the HAROS interface, through the use of report_metric and report_violation. 5.1. High-Assurance ROS 95 1from radon.visitors import ComplexityVisitor 2from radon.metrics import h_visit, mi_compute 3from radon.raw import analyze 4 5# The plug-in's entry point; file by file analysis. 6# iface - the interface to communicate with HAROS 7# scope - a HAROS Source File (language should be Python) 8def file_analysis(iface, scope): 9with open(scope.path, "r") as f: 10 code = f.read() 11 cc = analyse_cc(iface, code) 12 lloc, ratio = analyse_raw_metrics(iface, code) 13 h = analyse_halstead_metrics(iface, code) 14 mi = mi_compute(h, cc, lloc, ratio) 15 iface.report_metric("maintainability_index", mi) 16 if mi < 20: 17 iface.report_violation("mi_below_20","MI of " +str(mi)) 18 if mi < 65: 19 iface.report_violation("mi_below_65","MI of " +str(mi)) 20 21 def analyse_cc(iface, code): 22 visitor = ComplexityVisitor.from_code(code) 23 for fin visitor.functions: 24 iface.report_metric("cyclomatic_complexity", 25 f.complexity, line=f.lineno, function=f.name, class_=f.classname) 26 if f.complexity > 10: 27 iface.report_violation("max_cyclomatic_complexity_10",str(f.complexity)) 28 if f.complexity > 15: 29 iface.report_violation("max_cyclomatic_complexity_15",str(f.complexity)) 30 return visitor.total_complexity 31 32 def analyse_raw_metrics(iface, code): 33 metrics = analyze(code) 34 iface.report_metric("lloc", metrics.lloc) 35 iface.report_metric("sloc", metrics.sloc) 36 # ... 37 return (metrics.lloc, ratio * 100) 38 39 def analyse_halstead_metrics(iface, code): 40 metrics = h_visit(code) 41 # ... 42 return metrics.volume Listing 5.5: Excerpt of the HAROS plug-in for the Radon Python tool. 5.2. ROS Metamodel and Model Extraction 96 5.2 ROS Metamodel and Model Extraction The previous overview of HAROS shows that, despite it being designed for the analysis of ROS systems, it did not incorporate much domain knowledge besides package structure, and did not perform any domain-specific analyses per se. As such, and considering our research on modelling ROS systems for domain-specific analysis (see Chapter 3), our first step to improve HAROS is to ensure that its internal data structures follow a rich and complete metamodel. To enhance it further, we then incorporate prototype model extraction components, based on the static analysis approach described in Section 3.3. This is our first technical contribution (as part of this thesis). It ultimately enables the ROS-specific analyses we aim for, and opens new possibilities for model-based plug-ins. 5.2.1 Changes to the HAROS Analyser One of the most important changes to the analyser was to implement data structures with a direct correspondence to our metamodel, presented in Section 3.2. Most of the file system structures, such as Packages and Source Files, were already in place. Runtime entities, such as Nodes and Configurations, on the other hand, had to be introduced from scratch. The notion of a Project – which was previously just a collection of packages – had to be refined to accomodate Configurations. To promote reusability between applications and compatibility with the Visualiser, all metamodel entities can be exported in JSON format. The workflow of the analyser is unchanged in many aspects. We have extended the tool’s options and modes of operation to enable model extraction. As mentioned, the process of model extraction has been implemented in accordance with the algorithm presented in Section 3.3. If enabled, extraction happens during the setup stage, after the source code indexing takes place – i.e., once HAROS has already built the file system part of the model. At the time of writing, the extraction process is not complete, although it covers most of the common use cases. There are some elements of the extensive ROS API (e.g., provided by standard packages, such as message_filters , but not by the C ++ or Python client libraries directly) that are not yet covered. We focused on implementing extractors for C ++ source code, more common amongst critical and low-level code in ROS, whereas the Python extractors were an external contribution (more on that in Chapter 9). For model extraction to take place, we inevitably require some user input. There is no fully automatic method to determine whether a launch file represents an application, or whether it should be used in conjunction with others. Since Configurations are part of our notion of Project, we extended HAROS’ project files – the user input it already required to build Projects in the first place. Consider Fictibot as an example. If we wanted to add, for instance, a Configuration corresponding to multiplexer.launch , one of the various launch files found in the fictibot_controller package, we would add a configurations section to the respective project file, as seen in Listing 5.6. Configurations are identified by a unique name, followed by a list of launch files. The order of the launch files is important – the model extraction process interprets files in the given order, as roslaunch would if actually launching the files. 5.2. ROS Metamodel and Model Extraction 97 1project: Fictibot 2packages: ["fictibot_drivers","fictibot_controller","fictibot_multiplex", "fictibot_msgs"] 3configurations: 4multiplex: 5launch: 6fictibot_controller/launch/multiplexer.launch Listing 5.6: Minimal project file for Fictibot with configurations. We reiterate how model extraction is not complete (especially when based on static analysis). Our proposed algorithm addresses this by allowing user-provided extraction hints. Hints can be partial (i.e., it is not necessary to specify the system, or any node, in full), and are also specified in the project file, under the respective Configuration. We follow the YAML syntax for hints defined in the metamodel (Chapter 3, Section 3.3). For the sake of an example, assume that we had to fix the message type of the Fictibot Controller’s publisher on the /controller_cmd topic. Listing 5.7 shows the resulting project file. 1project: Fictibot 2packages: ["fictibot_drivers","fictibot_controller","fictibot_multiplex", "fictibot_msgs"] 3configurations: 4multiplex: 5launch: 6fictibot_controller/launch/multiplexer.launch 7hints: 8nodes: 9/ficticontrol: 10 publishers: 11 -topic:"/controller_cmd" 12 msg_type:"std_msgs/Float64" Listing 5.7: Project file for Fictibot with a configuration and extraction hints. Parsing source code to extract a model can take some time, especially when parsing complex languages such as C ++ . To improve the overall performance of the extraction process, we enhanced HAROS with a (work in progress) built-in database of pre-parsed Nodes. It features Nodes that belong to well documented packages (e.g., diagnostic_aggregator , robot_state_publisher ), released in the official ROS distributions. Another justification for this database, besides performance, is that ROS favours the reuse of components, and third-party packages are often installed from binaries. As a consequence, source code may not be always available for such common packages, which would require users to specify the missing nodes via hints. Embedding this domain knowledge in HAROS itself is another step towards the completeness of the extracted models. At the time of writing, this database contains primitives (such as calls to advertise , subscribe , etc.) from nodes belonging to 14 packages, as shown in Table 2. To clarify, we registered standard primitives (e.g., advertise ) used by nodes that these packages make available (e.g., the static_transform_publisher node of the tf package). We did not register new primitives that the packages themselves may introduce, to be used directly in C ++ (as is the case with the message_filters package and its TimeSynchronizer , for example). The database contains entries spanning all 5.2. ROS Metamodel and Model Extraction 98 Table 2: Built-in parsing database for HAROS. Package Nodes Primitives controller_manager 1 5 diagnostic_aggregator 1 9 hector_mapping 1 29 husky_base 1 9 interactive_marker_twist_server 1 4 joy 1 5 lms1xx 1 3 move_base 1 20 nodelet 1 4 prosilica_camera 1 6 robot_localization 1 12 robot_state_publisher 2 18 teleop_twist_joy 1 9 tf 1 1 Total 15 134 ROS distributions, for each package, from Indigo Igloo up to Melodic Morenia. Table 2presents the number of unique entries; if a Node’s interface does not change from one distribution to another, it is not counted. At this point, we also introduce the possibility of specifying configuration-specific data for analysis plug-ins. Under each configuration, as shown in Listing 5.8, a subsection called plugin_data contains a mapping where keys are plug-in names (e.g., plugin1 , plugin2 ), and the values can be of any type, including lists and other key-value mappings. The values are passed directly to the respective plug-in and have no semantics for HAROS itself. 1project: Fictibot 2packages: [fictibot_drivers, fictibot_controller, fictibot_multiplex, fictibot_msgs] 3configurations: 4multiplex: 5launch: [fictibot_controller/launch/multiplexer.launch] 6plugin_data: 7plugin1: [arg1, arg2, arg3] 8plugin2: 9arg1: ... 10 arg2: ... 11 arg3: ... Listing 5.8: Project file for Fictibot with plug-in-specific input data. While the reporting stage of HAROS is mostly the same (except that it has to export Configuration data), the analysis stage was improved to allow plug-ins to perform model-based analysis. Namely, we added a new plug-in entry point for Configurations (besides the existing ones for files and packages). Since Configurations are runtime entities, and constitute a new analysis scope, we also extended the plug-in 5.2. ROS Metamodel and Model Extraction 99 interface with a new reporting function, specifically to report issues on runtime entities. A practical example on how to make use of this new plug-in entry point is given in Section 5.3. 5.2.2 Changes to the HAROS Visualiser Graphical data visualisation is arguably one of the most valuable tools for developers in terms of obtaining immediate feedback. This is one of the main driving principles behind the HAROS Visualiser. Having equipped the analyser with model extraction capabilities, the next logical step is to extend the Visualiser to display the extracted models. Graphical architecture models of ROS systems (or software systems in general) are useful for two purposes: (i) helping develpers validate the implementation; (ii) providing documentation assets for free. We extended the HAROS Visualiser with a Computation Graph visualisation component that renders a graph of a selected Configuration, where each graph node is a ROS Resource and the edges are the ROS Links between them. This component features individual Resource inspection (e.g., message type and traceability to the source) and visibility settings for different Resources. As an example, Figure 40 shows the rendering of the multiplex Configuration from Listing 5.6. White circles represent Nodes, whereas green circles represent Topics. Figure 40: Display of a Computation Graph in the HAROS Visualiser. One of the options of the Visualiser enables ROS parameters to be displayed in the graph. These are displayed as purple circles, and are disabled by default, since, in many cases, their numbers are overwhelming, making the graph unintelligible. Services are always displayed by default, just like topics, but with blue circles. This particular example does not feature any services, though. Figure 41 shows the same Configuration, but with parameters enabled and the /ficticontrol node selected. When a Resource is selected, only its direct links are drawn on the graph. In the previous graphs we can see that two topics are rendered with dashed lines. Dashed lines represent conditional entities – entities that, depending on some conditions (e.g., an if statement) might not be 5.2. ROS Metamodel and Model Extraction 100 Figure 41: Computation Graph with parameters shown. present in all instances of the Configuration. This is one of the advantages of using static analysis for model extraction. With dynamic analyses, determining conditional entities would require extensive instrumentation of all sources of code (i.e., instrumentation of traditional C++ and Python, but launch files too). The Visualiser provides an information panel for every entity in the graph, where users can easily determine traceability details and which conditions affect the entity. Figure 42 shows the details of one of the topics, where we can see that it is affected by one condition, in the random_controller.cpp file. Figure 42: Resource details and traceability information. The use of static analysis, as already discussed, sometimes faces limitations regarding name resolution. For highly dynamic values (e.g., read from parameters), it is impossible to fully determine the resulting ROS name of a topic, service or parameter. Our extraction process handles this by including the unresolved entities in the model regardless, and the Visualiser does so too. When a Resource name is unknown, it is represented with ‘ ? ’. Since all names are resolved in the example from the previous figures, we altered the source code of the Fictibot Random Controller slightly, so that its /stop_cmd topic (remapped to /normal_priority_stop in this Configuration) becomes unresolved. As shown in Figure 43, when the unresolved topic is selected, the Visualiser performs pattern matching to find suitable candidates, ensuring that the message types match (highlighted in orange in the graph). One of the main benefits of this feature is to aid users in defining correct extraction hints, to refine the extracted models. 5.3. A Simple Architectural Analysis Plug-in 101 Figure 43: Pattern matching for unresolved Resources. Lastly, since one of our additions to the analyser was a plug-in reporting feature specifically dedicated to runtime entities, it only makes sense that the Visualiser is able to display such issues. If there are available issues with a set of runtime entities to blame, users can select such issues from a drop down menu, and the graph is updated with red highlights on the entities. The highlights can be applied both to nodes and edges – i.e., to Resources or Links. Figure 44 in the next section illustrates this last feature. 5.3 A Simple Architectural Analysis Plug-in The previous section describes how we enhanced HAROS, to equip it with model extraction capabilities. Such capabilities, coupled with a new entry point for plug-ins focusing on Configurations, play a key role in enabling ROS-specific analysis. New approaches, stemming from a model-based approach, become now feasible, whereas previously, when relying solely on pure static or dynamic analysis, they would require a lot more effort. In this section, we will build a proof-of-concept plug-in, to demonstrate how model extraction can be harnessed. The intended plug-in is a query engine over the extracted Computation Graph to detect architectural issues. The idea behind it is not to impose (or to come up with) specific rules and checks, but rather to let users specify the rules they want to enforce over an architecture. A basic example of this (that is actually a common guideline in many systems) is to ensure that every topic has at most one publisher . This rule is quite reasonable because, without it, there is a risk of having two publishers flood a topic, without any means for the subscriber to tell which message belongs to which publisher. It is easy to see that, especially when handling sensor data, this would likely cause unexpected behaviour. 5.3. A Simple Architectural Analysis Plug-in 108 queries should pick up (Figure 44). These red flags are mostly concentrated on the Fictibot Random Controller, as shown in Figure 45. Namely, we can see: • an occurrence of one global ROS name (/normal_priority_stop); • two topics under conditional statements (/custom_noparam and custom_w_param); • a topic using an unbounded queue (/normal_priority_stop); • a topic using a queue of size 1 (/normal_priority_cmd); • four topics using messages of type std_msgs/Empty (the four stop topics around the Multiplexer). Figure 44: Computation Graph with query reports in the HAROS Visualiser. Highlighted is a Link with a queue of size 1. 5.3. A Simple Architectural Analysis Plug-in 109 Figure 45: Query reports in the HAROS Visualiser. 5.4. Summary 110 5.4 Summary In this chapter, we started by introducing HAROS, a plug-in driven framework for static analysis of ROS systems. Initially, this framework featured little domain knowledge of ROS systems, besides their package structure. Its plug-ins were also adaptations of analysis tools for general-purpose programming, useful for gathering quality metrics or checking compliance with certain coding conventions. Nonetheless, it had been used for a general quality study of the ROS ecosystem. Our main technical contributions to HAROS were the implementations of our proposed metamodel and model extraction algorithm (presented in Chapter 3). This improvement changed how HAROS fundamentally handles a ROS application, and enabled new, model-based capabilities for analysis plug-ins. Most importantly, with our contribution, HAROS plug-ins are now able to perform any kind of analysis or processing of the ROS Computation Graph at compile time. To demonstrate such capabilities, we implemented a simple plug-in based on an existing Python query engine. This plug-in differs from traditional analysis tools by not hard-coding any rules, but rather allowing users to define new checks over the architecture of a ROS system. 6 ONLINE RUNTIME VERIFICATION OF ROS APPLICATIONS One of the goals of this thesis is to design (and implement) property checking techniques, applied to the ROS domain, that could help us gather the necessary evidence to structure a dependability case. In the previous chapters, we paved the way for this goal by (i) establishing a metamodel for ROS applications; (ii) defining a language to annonate models with behavioural properties; and (iii) by enhancing an existing ROS analysis framework with model extraction capabilities. We have demonstrated, in Chapter 5, how architectural properties can be validated. In this chapter we address the challenge of providing evidence that a system’s behaviour complies with its behavioural specification. Up to this point, we built a foundation mostly on static analysis. To analyse how a ROS system behaves at runtime, we propose an approach based on dynamic analysis instead. Namely, we propose using Runtime Verification to detect violations of MFOTL formulae (restricted to the subset defined by our specification language in Chapter 4). While Runtime Verification is not a novel concept in the ROS ecosystem, our approach is the first to be both based on a high-level, pattern-oriented specification language, and on Metric First-Order Temporal Logic. It is integrated in the HAROS framework via a plug-in that generates the appropriate runtime monitors for a given Configuration and its behavioural specification. Furthermore, this Runtime Verification approach will provide a foundation for other techniques to build upon, as we will see in Chapter 7. 6.1 State of the Art Runtime Verification is a verification technique that revolves around the use of monitors to observe a system’s execution, in terms of its internal or external operations. As with any verification technique, the goal is to determine whether the system under observation satisfies or violates a given correctness property . The main advantages of this technique are that it is relatively lightweight, and that it acts on a system implementation, rather than a model. The domain of Runtime Verification is a vast research topic. There are many approaches to it, and they vary wildly with regards to, e.g., how monitors observe a system, whether they interfere with said system, or how timely is their detection ability. Some taxonomies have been proposed to address this matter. We start this section by presenting the different types of Runtime Verification. Then, we discuss the existing 111 6.1. State of the Art 112 tools and algorithms that relate the most to our own approach. More concretely, we are interested in the state of the art in Online Monitoring . 6.1.1 Taxonomies for Runtime Verification Cassar et al. [ 42 ] focus on the distinction between Offline Monitoring and Online Monitoring . They consider the former as its own category, and then spread Online Monitoring across a spectrum of Completely-synchronous Monitoring (CS) , Synchronous Monitoring with Synchronous Instrumentation (SMSI) , Asynchronous Monitoring with Checkpoints (AMC) , Asynchronous Monitoring with Synchronous Detection (AMSD) and Completely-asynchronous Monitoring (CA) . O f f l i n e M o n i t o r i n g The offline approach is completely decoupled and independent from the system under observation. Typically, an execution (i.e., a trace) of the system is recorded and persisted inside a data store – for instance, as a log file. The trace may contain a full execution of the system, or it can be partial, but either way it is finite. The monitoring solution then processes the stored trace and determines whether it satisfies the specified properties. One of the main advantages of this type of monitor is that it can view the system’s execution as a whole, and it can traverse the trace multiple times, both forwards and backwards. The obvious price of such decoupling and flexibility is late detection – when a violation is detected, it is too late to act. Cassar et al. deem Offline Monitoring especially suitable to double check the behaviour of systems that already have a high correctness confidence. O n l i n e M o n i t o r i n g The online approach, as implied by its name, is the exact opposite of Offline Monitoring. A system is monitored during its execution – meaning that monitors have to run alongside the system (or as part of it). The most immediate advantage is that violations can be detected earlier, and, sometimes, monitors can even preempt the system from causing harm or entering an error state. This is essentially mandatory for safety-critical systems and for security purposes. In exchange, the monitoring algorithms tend to be more complex (the trace is observed incrementally) and the monitors themselves may impact the system’s performance. Cassar et al. had in consideration the different levels of coupling between an online monitor and its monitored system, and categorised the existing approaches as follows. CS Completely-synchronous monitors operate hand in hand with the system. In this tighly coupled and highly intrusive approach, the system as a whole blocks every time the monitors process an event. In the same fashion, when a violation is detected the whole system is affected (e.g., brought down). The inevitable performance overhead is the cost of having the earliest possible detection. This all-or-nothing stance is common in monolithic or embedded systems. SMSI Synchronous Monitoring with Synchronous Instrumentation is a level only slightly less intrusive than Completely-synchronous Monitoring. The main difference between the two, is that SMSI only blocks the component whose event is being processed, letting other components execute freely. 6.1. State of the Art 113 AMC Asynchronous Monitoring with Checkpoints is the middle ground approach. Monitors are sufficiently decoupled for events to be processed asynchronously, but, after reaching a checkpoint (e.g., during a light load period), the system blocks, waiting for the monitors to catch up. With AMC, it is possible for users to strike a balance between timely detection (e.g., for safety-critical events), intrusiveness and performance overhead – provided that checkpoints are properly configured. AMSD Asynchronous Monitoring with Synchronous Detection is another intermediate approach. It behaves mostly as a completely-asynchronous solution, but events that may directly contribute to a violation are marked as critical events. After a critical event is sent to the monitor, the associated component blocks, waiting for the monitor’s verdict. CA Completely-asynchronous monitors are the most efficient of all. They are loosely coupled, requiring only minimal instrumentation to listen to events. Event handling is done in the background, leaving the system free to proceed with its execution. The obvious price to pay for increased efficiency is late detection. As such, it is not an ideal solution for monitors to take preventive or mitigating measures upon detecting a violation. In this sense, it is similar to Offline Monitoring, with the main difference being the incremental monitoring nature of CA – it does not require a pre-recorded trace. A more extensive taxonomy is proposed in [ 62 ]. Falcone et al. classify Runtime Verification tools not only in terms of Online versus Offline monitoring, but rather by taking into account seven parameters. Namely, they propose a taxonomy driven by: specification and monitor traits; deployment (implementation) of the monitor; how traces are modelled and observed; the monitor’s reaction to violations; the level of interference with the monitored system; and, lastly, by the application area of the runtime verification tool. S p e c i f i c a t i o n A specification encodes the properties that one wants to verify. It exists within the context of a system model, and is often designed prior to running the system itself. Falcone et al. distinguish specifications based on whether they are implicit or explicit . The former do not require user input, and could be used to capture general errors that lay beyond the compiler’s ability, such as ensuring memory safety or the absence of deadlocks. The latter, provided by the user, is a formal encoding of functional or non-functional requirements of the system. Its main traits are: the expected output (Booleans, witnesses, streams); the encoding paradigm (declarative or operational); the supported modalities (current, past or future); how data is handled (propositional vs. parametric observations); and its concept of time (totally-ordered or partially-ordered logical time vs. discrete or dense physical time). M o n itor Monitors are among the main components of a Runtime Verification framework – they enable the observation of a running system and decide whether a property is satisfied or violated. Monitors are categorised by their decision procedure , execution and generation . Decisions can be analytical – by querying and scanning records – or operational – using automata or formula rewriting to reach a verdict. Furthermore, the procedures are distinguished by whether they are sound, complete or impartial, and whether they use behaviour prediction or anticipation. Monitors can be explicitly or implicitly generated, 6.1. State of the Art 114 and then directly executed or interpreted – based on whether they are implemented in their own piece of code, rather than being made up of parameters for a general monitoring infrastructure. D e p loymen t This category refers to how monitors are implemented in practice, and how and when they observe the target system. The deployment stage distinguishes whether the monitor acts offline or online. In the case of online monitoring, the authors distinguish only between synchronous and asynchronous monitoring. The placement of the monitor is said to be inline if the monitor runs as part of an instrumented system, or outline if it runs as a separate entity, with a dedicated means to receive observations. Deployment information also considers the architecture of the monitor, distinguishing between centralised architectures and decentralised ones. R e a c t i o n A monitor’s reaction to observations is either active or passive . The former is able to affect the monitored system directly, for instance by preventing violations from happening, or, if a violation happens, by taking recovery measures, raising exceptions or rolling the system back to a previous state. A passive monitor does not affect the running system. It is a simple observer, concerned with producing the designated specification output, various statistics or explanations for outputs (e.g., a witness trace for a violation). T r a c e Traces are another key concept to Runtime Verification. Falcone et al. note that there is a distinction to be made between the trace model used in the specification, and the actual observed trace (i.e., the monitor’s abstraction). A model could be infinite, but an observed trace is finite by definition. Monitors can sample the observed trace based on events or on time (e.g., periodic snapshots). Observations can be precise or imprecise. The information contained in a trace also varies. Some traces contain only events, while others can include internal system states, signals (for time-continuous information), and input-output operations. All monitored information represents an evaluation of the system’s state, which could be relative to a point or to an interval. I n t e r f e r e n c e Interference is measured on a spectrum, between invasive and non-invasive . A monitor can never be completely non-invasive (even in offline monitoring), due to the overhead of instrumentation, to collect the trace. The degree of interference changes depending on multiple factors, but online monitors (especially with an active reaction) tend to be more invasive. A p p l i c a t i o n A r e a The application area of Runtime Verification mainly portraits its purpose. A few example areas include collecting information , testing , debugging , failure prevention , recovery and various safety , security and liveness analyses. Francalanza et al. study Runtime Verification in the context of decentralised and distributed systems [ 68 ] (of which ROS is an example). When monitoring such systems, one has to face a few challenges that are not intrinsic to the simpler non-distributed programs. In particular, they emphasise the challenges of: 6.1. State of the Art 115 • fault tolerance , as many monitoring approaches do not consider the independent failures of different nodes; • global atomic observations , which are hard to achieve when predicates can, potentially, refer to distinct parts of the system; • monitor orchestration , i.e., how to optimally distribute monitors over a network; and • monitorability and correctness , given that decentralised and distributed systems impose even more restrictions on runtime analysis than non-distributed systems (e.g., non-determinism). As noted by Francalanza et al., there are multiple possible approaches to these problems. They review the state of the art on distributed monitoring, and classify existing approaches mostly based on (i) whether there is a single central monitor or the monitoring task is distributed; (ii) whether there is an assumption on a global clock; (iii) whether the monitoring system tolerates failures; and (iv) its intrusiveness. Regarding (i) , the matter of monitor organisation , their classification includes the following four classes. T r a d i t i o n a l M o n i t o r i n g This is the simplest, most straightforward approach to monitoring. In this setup, there is a single, central monitor that observes the various processes scattered over the distributed system. Its main advantage is that it always reports a trace with a total ordering of events, despite the many possible interleavings of the monitored processes. However, it suffers from increased overhead, sub-optimal efficiency, worse tolerance to faults and weaker security. D e c e n t r a l i s e d M o n i t o r i n g The decentralised setup is the first step towards distribution, from traditional monitoring. The specification is broken down in multiple monitors, which may reside in different locations of the system, to perform local observations and build a single synchronised trace. Monitors are not required to interact among themselves, and they assume the existence of a global clock and a total order over all computations. The decomposition of a specification sometimes emerges naturally, when sub-properties pertain to different nodes. O r c h e s t r a t e d M o n i t o r i n g Orchestration is useful when more than one process resides in multiple locations of the system. In this setting, a trace is produced for every location in the system, based on local observations, without synchronisation or the assumption of a global clock. Monitors are central (i.e., one monitor per correctness property) and live in a remote location, where they gather and merge the local traces to produce a verdict. Centralisation trades scalability, in the form of increased communication overhead, and security, augmenting the risk of data exposure, for simplified monitor logic. C h o r e o g r a p h e d M o n i t o r i n g This setup is similar to Orchestrated Monitoring, in the sense that traces are produced at the location of the processes, based on local observations without synchronisation. The main difference is monitor distribution. Monitors are placed at the same locations as the processes, making direct observations over the local traces, but they are allowed to synchronise with each other to obtain remote information. This approach often requires less communication than the orchestrated 6.1. State of the Art 116 approach, having its main drawback in the complexity of the implementation and instrumentation of the monitored system, as well as being more intrusive in general. 6.1.2 Runtime Verification Tools and Algorithms Numerous runtime verification tools and algorithms have been proposed, for all sorts of specification languages and application areas. In this section, we provide an overview of some of the most relevant approaches for our context – distributed, message-passing systems, preferably in the domains of ROS or robotics in general. Our goal is to employ runtime verification for the specification language we presented in Chapter 4, so there are a few attributes that are of particular interest to us, such as handling specifications with parametric data and physical time. As previously mentioned, the research topic of runtime verification for distributed or decentralised systems is a challenging one. One notorious challenge is the possibility of network failures. Basin et al. address this issue [ 19 ] and propose the first monitoring algorithm that is able to tolerate such failures as well as being able to handle out-of-order messages. Their specification language is based on three-valued Metric Temporal Logic, which is able to handle time constraints, but is limited to propositional events. Mostafa and Bonakdarpour propose the first runtime verification algorithm for asynchronous distributed programs that is both sound and complete [ 126 ], without assuming the existence of a global clock (a consequence of asynchrony). They base their specification language on three-valued LTL defined over the global state of the distributed program. A distributed program, in this context, is considered to be a set of asynchronous processes that communicate using message-passing primitives over reliable channels. A ROS system, for instance, would qualify for this definition. The algorithm is able to verify temporal properties beyond safety predicates, and is inspired by distributed computation slicing – the technique of abstracting distributed computations with respect to a given predicate. It is fully decentralised, in the sense that each process maintains a replica of a monitoring automaton (an intrusive approach). Each monitor deals with concurrent events by maintaining a set of all possible verdicts for a given predicate. This approach was evaluated on a simulated swarm of flying drones, and the authors found that the monitoring overhead grows only in the linear order of the number of processes and events. DecentMon [ 21 ] is a monitoring tool for LTL specifications over decentralised systems, such as circuits and embedded systems, where there are multiple parallel components working in synchrony (i.e., a global clock can be assumed). DecentMon takes as input multiple traces of the system and an LTL formula. Formulae are then monitored in two different modes: 1. traditional monitoring, where a central monitor merges the input traces into a single, global trace; or 2. decentralised monitoring, where each trace is read by an individual monitor. ARTiMon [ 145 ] is a monitoring tool that specialises in handling time. It was historically developed for online validation of Matlab and Simulink models, but it evolved to more general applications. In ARTiMon, the monitored system is viewed as a set of state variables and a time domain (either discrete or continuous). It interprets all terms of its input language as partial time functions over the time domain. The specification 6.1. State of the Art 117 language itself includes a few interesting features, such as temporal operators with interval bounds, the ability to aggregate values, and the ability to refer to the last observed value or the previous value for a given event. One of its drawbacks is that the specification language only considers primitive data types. Complex data types are not supported, and, thus, other features such as quantification are also left aside. ARTiMon monitors are implicitly generated and of interpreted execution. While ARTiMon specialises in time, DejaVu [ 81 ] focuses more on data. It is a monitoring tool for First-Order Temporal Logic specifications with a past modality over events that carry data, that uses Binary Decision Diagrams (BDDs) to represent and manipulate observed data. This data structure comes with a few advantages, namely in terms of highly compact data representations and being highly efficient for a number of operations. The authors note that the monitor construction procedure for the propositional case naturally extends to BDDs, which comes as an added benefit for this choice. R2U2 [ 153 ] is a runtime verification system specifically designed to monitor and diagnose security threats for unmanned aerial vehicles (UAVs). In safety-critical systems, such as UAVs, both software and hardware present potential threats and faulty components. Thus, R2U2 is proposed as a solution to verify hardware safety and software security properties, by monitoring system health and finding possible attack patterns. It is not generally applicable in other contexts, as it is implemented on its own hardware, as a hardware and software bus traffic observer. Despite this major drawback, this design decision achieves extra protection against attacks, and reduces obtrusiveness to a minimum. Kane et al. present a case study on online monitoring of an autonomous research vehicle (ARV) system [ 92 ]. Their work addresses an important problem in safety-critical systems – that, often, these systems feature a number of black-box, commercial-off-the-shelf components. Without full access to the source code, runtime verification approaches based on instrumentation become unfeasible. Furthermore, ARV systems tend to be hard real-time, in which case instrumentation is neither available nor without an impact in performace. They propose a passive monitoring algorithm, called EgMon , that observes exchanged messages over a Controller Area Network (CAN) – a standard broadcast bus for ground vehicles. Properties are written in future-bounded, propositional Metric Temporal Logic, in order to handle timing related properties (which they deem to be common in this context 1 ). The EgMon algorithm incrementally takes as input a system state (defined as a mapping Proposition ↦ {⊤,⊥} ) and a MTL formula and eagerly checks the state trace for violations. EgMon’s eager approach, based on dynamic programming techniques, aims to reduce the input formula as soon as possible using history summarising structures and formula-rewriting. TeSSLa [ 51 ] takes on a different approach regarding runtime verification. Whereas most tools and specification languages are event based, TeSSLa focuses on stream based runtime verification. Stream based verification, as implied by the name, treats input data as continuous streams, or signals (although TeSSLa also handles sparse, event-based data under the same formalism). In cyber-physical systems, this is a common notion that nicely captures, e.g., very frequent sensor readings. In essence, TeSSLa is just a mechanism to transform input streams into output streams. Specifications define stream transformations, 1 As an example, the authors note that many properties in ARVs follow the pattern “the system must perform action 𝛼 within 𝜏 seconds of event 𝜀 ” . This could be captured by our specification language as “globally:𝜀causes 𝛼within (𝜏 × 1000) ms”. 6.3. Approach Overview 124 Also related to the theme of late detection is MonPoly’s focus on safety (and co-safety) properties. As MonPoly negates the input formula and looks for a counterexample, it can only focus on detecting violations. For properties such as ‘ globally:some /b within 1000 ms ’, MonPoly will always take one second to produce a verdict: after one second, either b() was observed or it was not. There is no reliable way to detect early success. The workaround is to run two monitors, one that looks for a violation, as normal – i.e., verifying ∀𝑥 ∶ ♦[0,1000)b – and another that does not negate its input formula – i.e., one that treats the desired event, b() as the violation and verifies ∀𝑥 ∶ [0,1000)¬b . Once a b() event is detected by the second monitor, both monitors can be safely interrupted. Finally, there are smaller, technical obstacles for the direct adoption of MonPoly. The most immediate one is that the tool is implemented in OCaml, and ROS does not provide any official bindings for the OCaml language. We would have to resort to unofficial bindings, or use the tool as a child process of a ROS node. Inter-process communication is, naturally, slower than using a single process, which further contributes to detection latency. Weighting all these factors, we have decided not to adopt ParTraP or MonPoly but, rather, to implement our own Runtime Verification algorithm, tailored for our specification language. Regardless, we did put MonPoly to the test, and compared its performance against the approach we propose in this chapter. This evaluation can be found in Chapter 8, Section 8.3. 6.3 Approach Overview We have seen how, according to Falcone et al.’s taxonomy [ 62 ], a Runtime Verification approach can be categorised with respect to seven parameters, namely: the specification, the monitor, the deployment process, the monitor’s reaction, the monitored trace, monitor interference, and application area. We are able to identify our stance, right away, in terms of application area, property specification, monitored traces and the monitor’s reaction. A p p l i c a t i o n A Runtime Verification solution can have many potential application areas. In general, one could argue that the main application of our approach is debugging . In Chapter 7, we show how our approach can be used for testing too. Specification Weuse explicit specifications , seeing as we provide a declarative language tailored for this purpose. This language supports past, current and future observation modalities; handles complex, parametric events with quantification; and is able to express logical time constraints with total order, and physical time constraints with discrete time. In terms of output, the specification and monitors themselves aim to produce only a verdict . Within the larger scope of Property-based Testing (see Chapter 7), for instance, we can add a witness as well. T r a c e We presented a specification language based on infinite trace models . During execution, trace observation should be event triggered (as we are dealing with the observation of ROS messages) and 6.3. Approach Overview 125 precise – monitors observe every new event of interest. Trace evaluation should be done at specific points, such as when a new message is observed or when a timer expires. R e a c t i o n Monitors, regardless of their implementation, should have a passive reaction , i.e., they should be limited to reporting verdicts. Our specification language does not allow the encoding of actions, unlike, e.g., DeRoS. Moreover, a passive reaction is the most flexible approach to use runtime monitoring as a building block for other purposes. For example, consider the testing approach we present in Chapter 7. If the runtime monitors were allowed an active reaction, it could possibly interfere with the system’s behaviour and, consequently, with the test results. The other parameters essentially dictate how we will approach the monitor implementation, and will be discussed in the remainder of this section. 6.3.1 Generation and Execution The first design problem we face regarding runtime monitors is how to generate them. The taxonomy offers two possibilities, explicit generation or implicit generation . Design Problem 1. Should monitors be explicitly generated from the specification, or should they exist implicitly as part of a general monitoring system? Another way to put this question is to ask whether we want to have a tailor-made monitor for each property, or whether we want to implement a generic monitoring solution, able to handle all types of properties of our specification language. MonPoly, as we have seen, is an example of the latter. It exists as a generic monitoring tool for a subset of Metric First-Order Temporal Logic. In our case, we believe that explicit generation is the better option. We have a limited specification language, with a number of patterns that we know ahead of time. As such, we can design a custom monitor for each of the available patterns. Then, we can optimise each type of monitor individually. This is one of the aspects MonPoly lacked in our previous analysis. For some formulae, MonPoly has no option but to wait until the end of the trace (or the end of the specified temporal bound) to produce a verdict. There is no reliable way to detect early success of an Existence property, for instance. By building a monitor that is tailor-made for a given type of property, we can benefit from the earliest possible detection. One of the disadvantages of working with a domain-specific specification language is its reduced maintainability. The generation process is tied to this language. If the language evolves, to address issues or to introduce new features, such changes could have an impact in the whole generation process. Regardless of how monitors are generated, deciding how monitors are executed is also a binary problem. Design Problem 2. Should monitors have their own piece of code to execute (direct execution) or should a generic algorithm be parameterised to handle individual properties (interpreted execution)? Monitor execution sounds as a problem that is related to monitor generation, but the two are actually independent problems. We have decided to explicitly generate monitors, but we have not yet decided 6.3. Approach Overview 126 on what a monitor is. In other words, we have to decide what is the output of the generation process. A monitor could be a set of parameters for a generic algorithm (e.g., the states and transitions of an automaton), which is then interpreted, or it could be code that is directly executed. Taking MonPoly for comparison, it uses an implicit generation process (i.e., the monitors are produced internally) with interpreted execution. The input MFOTL formulae are converted into first-order queries (the monitors) and then used to parameterise the generic monitoring algorithm. In our case, the two options boil down, essentially, to the following: 1. direct execution – each property is synthesized into a full-blown monitor implementation (i.e., code), where every variable is hard-coded in the output; 2. interpreted execution – we provide the user with a standalone, generic monitor implementation for each pattern (i.e., a monitor for Absence properties, a monitor for Existence properties, etc.), which is then parameterised with information that is specific to each monitorable property (the result of the generation process, e.g., topic names, predicates over messages or timeouts). Either option works. In order to tip the scales, we view this problem from the perspective of the HAROS framework. HAROS is used for the whole process that leads to monitor generation, from the initial specification to producing an annotated model. It makes sense that monitor generation should be implemented as a plug-in for the framework. Using our new entry point for the analysis of Configurations (see Chapter 5), we can take each annotated Configuration individually, and then generate the appropriate monitors. Configurations are needed, in addition to the properties, in order to provide type information, such as the expected message types of each topic. HAROS can also perform sanity checks on the specified properties, e.g., to ensure that they refer to message fields that actually exist. In this context, we believe that direct execution is more appropriate. Instead of having the plug-in generate a set of parameters for the user to plug into an external monitor implementation, we can produce the whole monitor in one go. It is the most portable solution, and allows for greater freedom when it comes to optimisation. As for the technical aspects of monitor generation, we use metaprogramming and a template engine. Template engines, such as Jinja 6 , are similar to compilers or transpilers, in the sense that they take source code as input to produce an output (typically source code). In this case, the input source is a template , i.e., an arbitrary source file, similar in content and structure to the intended output (e.g., Python, C ++ , etc.), in which users can insert variable points, using a mini-language provided by the engine. Given a template and concrete values for each variable, the engine performs the replacement step to produce the output file. In a way, they are more powerful versions of the same mechanisms that support format strings , such as: 1x = 1; y = 2 2text = '{c} = {a} + {b}'.format(c=(x+y), a=x, b=y) 3print(text) The main difference is that Jinja (and other template engines) support complex features embedded within this template language, such as conditionals, loops, nested templates and template inheritance, to name a 6https://palletsprojects.com/p/jinja/ 6.3. Approach Overview 127 Figure 46: Workflow of the proposed Runtime Verification HAROS plug-in. few. Figure 46 shows a high-level view of the integrated workflow within HAROS, from specifications to monitor generation using Jinja templates. 6.3.2 Deployment An online monitor is a component that runs alongside a monitored system (or as part of it) for the purposes of the runtime verification process. But there are various methods to integrate the monitor with the system, various ways to observe execution traces, and various degrees of interference with the monitored system. Online monitoring will always have some degree of interference, due to the additional runtime overhead of running the monitors. However, depending on the other choices we make, this interference can be alleviated to an extent. The most immediate question is where do the generated monitors go, or, rather, where are they placed in the ROS computation graph. Design Problem 3. Should the generated monitors run alongside the ROS system (outline monitoring) or as an extension to the existing nodes (i.e., instrumentation, or inline monitoring)? In essence, we are deciding whether the monitor generation plug-in produces a standalone (outline) piece of code that executes alongside the ROS system, or whether it inlines the generated monitor in the existing nodes, producing an altered (instrumented) version of the system. There is a grey area in which the monitor runs as a separate entity, but some instrumentation is still applied to the system to report events to the monitor. Inlining is a common practice, especially in single-process software, as it is the closest a monitor can get to the monitored system. It makes observation of events easier and allows for the earliest possible 6.3. Approach Overview 128 detection. It is also a great choice for monitors with an active reaction. The major drawbacks are the increased level of interference, and the requirement of an editable version of the system to instrument – it must alter, e.g., the system’s source code or other intermediate representations, such as bytecode. This is not always feasible for various reasons. The target system might be encrypted, might be executing remotely, or it might just be a matter of user permissions. For ROS, in particular, we deem inlining to be a poor choice for a few reasons. 1. ROS applications are distributed by definition. It is possible for a single property to refer to topics that are advertised by multiple nodes. For inlining to work, in general, we would be forced into a distributed monitor architecture, which raises a number of other questions and obstacles. 2. It is unlikely for users to have access to the source code of all the components that make up the system. After all, one of the core philosophies of ROS is component reuse and, in many cases, reused components are installed as pre-compiled binaries, not as source code. 3. In the context of HAROS, we might be working with Configuration models for which there is neither source code nor pre-compiled binaries to instrument. For instance, we could be using models completely built by hand, or we could set up HAROS to run on a machine other than the machines used for development, such as a remote server. Outline solutions, i.e., monitors that run as their own entities, are more flexible in the ways they can handle the obstacles above. Distribution of the ROS application, for example, can be tackled both with a distributed monitor architecture and with a centralised monitor architecture, provided there is some interface through which monitors are able to observe all necessary messages. The existence of source code (or lack thereof) might not a problem either, depending on how we approach the observation of events, which leads us to the next question. Design Problem 4. Should monitors observe messages directly (i.e., should they subscribe topics on their own, and thus register themselves as ROS nodes), or should the monitored system be instrumented to log events, such as publishing or receiving a message, for external monitors to use? This question determines whether we opt for a pure outline solution, or whether we fall into the grey area, using instrumentation to report events, but not to evaluate formulae. The mixed approach is ideal to achieve soundness of the decision procedure, as we will discuss later in this section. However, for the reasons listed previously, regarding inlining, it might not always be feasible. In constrast, outline monitors with no instrumentation, i.e., ROS nodes that passively observe the system, can always be generated and deployed. This, in conjunction with a few other advantages, led us to choose the outline approach. First, outline monitoring nodes can always be generated and deployed because this approach works out-of-the-box with any ROS system. The system is, for all purposes, a black-box with exposed topics, regardless of whether it actually exists or of its current state of development. Monitoring nodes can be generated based on the specification. This decoupled stance is especially appealing in a few circumstances. For example, in the context of HAROS, we want to minimise any restrictions on the systems we are able to analyse, when possible. 6.3. Approach Overview 129 Second, the implementation is simpler, since it does not rely on instrumentation. Neither does it rely on dynamic changes to the ROS environment, such as replacing the ROS Master, providing wrappers for the ROS client libraries, or injecting men-in-the-middle nodes (e.g., as seen in ROSRV [ 85 ]). The monitored ROS system is left as it is. We have only to put together a template for an independent node, that, like many other ROS tools, uses the standard ROS interfaces to observe messages and perform its job. Third, and related to the previous point, it is the least intrusive option. Since the implementation of the monitored system is not tampered with, this approach has no effect on the non-functional performance of the monitored nodes. This is an important point; if a node experiences decreased non-functional performance, it can suddenly miss deadlines that it would not otherwise. Missed deadlines in one node mean false assumptions and late (or stale) data for another node, which could ultimately spiral into a system-wide failure. For instance, it is common for sensor nodes (such as laser scanners) to state their publication rate up front in the device documentation. If the overhead of a monitor causes the sensor to skip a message, client nodes (e.g., mapping and localisation) that assume this frequency might misbehave, and cause the robot’s model of the world to start diverging from reality. Over time, these small divergences accumulate and cause unexpected behaviour. One could argue that there is overhead in simply running the monitoring system alongside the ROS application, but, since nodes run in independent processes, the risk is smaller. In the worst case, the monitoring nodes could be moved to a separate machine in the ROS network, exchanging performance overhead for late detection – which leads us to another discussion. 6.3.3 Architecture and Orchestration One of the downsides of implementing outline monitors as ROS nodes that subscribe topics on their own is late detection. In this case, monitors have to be completely asynchronous (as per the taxonomy in [ 42 ]), and completely asynchronous monitors are known to suffer from late detection, in exchange for being the most efficient. Without instrumentation, there is no way to block the system and have it wait for the monitors, so any synchronous or partially synchronous approach is out of the question. These monitors are not ideal to take an active stance (e.g., for system repair), but, as we previously stated, that is not our main goal with this Runtime Verification approach. And, while detection might be late, it is still not as late as with offline monitoring; there is some utility in it to explore. The degree of latency to which monitors are subject is a variable that we can manipulate to some extent. Our choices regarding monitor architecture, orchestration and distribution may be a contributing (or dampening) factor. But, as noted by Francalanza et al. [ 68 ], distributed systems, such as ROS systems, face an increased number of challenges, in particular regarding fault tolerance, correctness and global atomic observations. Thus, lies our next question. Design Problem 5. Should monitors be monolithic (i.e., a traditional monitoring approach, with a single central monitor), or should they be distributed over the network (possibly addressing different parts of the specification)? 6.3. Approach Overview 130 Choreographed , orchestrated and decentralised monitors take advantage of local observations, when a system is spread over multiple network locations. In theory, they can be more efficient than a traditional approach. In a ROS setting, however, nodes tend to live in a reduced number of locations (possibly a single machine), with the notable exception being robot swarms. Even so, spreading monitors over multiple machines in a network would only make a difference for high-frequency publishing between nodes living in the same machine (to decrease the latency of the monitor). As such, we deem the increased complexity of distributed solutions unnecessary and opt for a traditional monitoring approach, with a centralised architecture. To further reinforce this position, one of the goals of ROS is to abstract away the network layers and focus on messages, after all. ROS nodes are allowed to subscribe any number of topics, and are able to use a global clock by default (in the form of the rostime interface), further discouraging monitor distribution and making the assumption of such a clock (and a total ordering of events) trivial. Furthermore, our specifications are not easily prone to decomposition. There are not many circumstances in which we might be actively looking for concurrent events (for a single property), and the addition of references to past messages adds another layer of complexity to the monitor implementation. Implementing a generation process that produces a monolithic ROS node (per property) is also convenient to make verdicts available, both to the user and to other components. Once the monitor reaches a verdict, of either ⊤ or ⊥ , regarding the system’s compliance with the monitored property, it can simply publish the verdict as a boolean ROS message. Thus, each monitor should advertise a verdict topic under its private namespace, so that the verdicts for each property are both easily accessible, as well as easily distinguishable. For instance, if we have two monitor nodes, /monitor1 and /monitor2 , we would also have two verdict topics, under the ROS names /monitor1/verdict and /monitor2/verdict . Components that build on top of this Runtime Verification approach can, then, selectively listen for the verdicts that are relevant to them. With this is mind, there is only one more item to discuss: monitor semantics, or how monitors reach verdicts. 6.3.4 Semantics The final design problem, now closer to the algorithm itself, is related to the monitor’s decision procedure. Design Problem 6. What kind of decision procedure should monitors adopt? Analytical decision procedures, such as querying records, are better suited for an offline monitoring approach, rather than online monitors. Between the different operational procedures, we opt for an automata-based monitor . Given that our specification language covers different states of the system and their transitions – e.g., entering a scope or triggering a Response pattern – automata are the most direct implementation. The semantics of this decision procedure are mostly the same as the semantics we presented in Chapter 4, for the specification language, with one caveat. We defined the semantics of the specification language based on infinite traces. Online monitors can be based on the concept of infinite traces, even 6.3. Approach Overview 131 though they always operate on a finite trace prefix – the finite number of events that have been observed, up to a certain point in time. The first thing we have to do is to define what is a finite trace prefix. Traces can be defined in terms of temporal first-order structures, as follows. Definition 5. Let (𝐷,𝜏) be a temporal first-order structure over signature 𝑆 , with 𝐷 = (𝐷0,𝐷1, …) a sequence of structures over 𝑆 and 𝜏 = (𝜏0, 𝜏1,…) a sequence of natural numbers (time stamps). Given 𝑘 ∈ ℕ0 , we define the 𝑘 -prefix of (𝐷,𝜏) as the pair (𝐷[0,𝑘),𝜏[0,𝑘)) , where 𝐷[0,𝑘) = (𝐷0,𝐷1, … , 𝐷𝑘−1) and 𝜏[0,𝑘) = (𝜏0,𝜏1, … , 𝜏𝑘−1) are finite sequences of size 𝑘 . According to this definition, at the initial instant the monitor is operating on a 0-prefix, i.e., it has not observed any events yet. As soon as it observes the first event, it operates on a 1-prefix trace. Note that this is not a prefix of any particular trace. We know that, theoretically, there is only a single trace of execution. In practice, at any given instant, we have only access to a 𝑘 -prefix, for some 𝑘 , which is a valid 𝑘 -prefix for an infinite number of infinite traces – we cannot predict the future. However, we must be able to query the monitor’s verdict at any given time. Monitors do not run for an infinite amount of time, neither does the monitored system. Intuition also says that, in many cases, we should be able to tell that a violation occurred as soon as it is observed. In order to be able to assign a verdict to each state of the generated automata, we use a three-valued variant of MFOTL, similar to other three-valued variants of temporal logics commonly used in Runtime Verification (see, for instance, [ 23 ]). Formally, we define the semantics of the runtime monitors in terms of the semantics given in Chapter 4, as follows. Definition 6. Let 𝑘 ∈ ℕ0 and (𝐷[0,𝑘),𝜏[0,𝑘)) be a 𝑘 -prefix of a temporal structure over 𝑆 . Let 𝑣 be a valuation, 𝑖 ∈ ℕ0 and Φ be a property over 𝑆 . We define (𝐷[0,𝑘),𝜏[0,𝑘), 𝑣, 𝑖) ⊨ Φ as • ⊤ iff, for all (𝐷′,𝜏′) temporal structures over 𝑆 , (𝐷[0,𝑘),𝜏[0,𝑘)) is a 𝑘 -prefix of (𝐷′,𝜏′) and (𝐷′,𝜏′, 𝑣, 𝑖) ⊨ Φ ; • ⊥ iff, for all (𝐷′,𝜏′) temporal structures over 𝑆 , (𝐷[0,𝑘),𝜏[0,𝑘)) is a 𝑘 -prefix of (𝐷′,𝜏′) and (𝐷′,𝜏′, 𝑣, 𝑖) ⊭ Φ ; • ? (or unknown) otherwise. Informally speaking, a runtime monitor has the following three possible outcomes. TRUE if and only if, for all possible continuations of the observed trace prefix, the property is always true; i.e., a good prefix has been already observed. FALSE if and only if, for all possible continuations of the observed trace prefix, the property is always false; i.e., a bad prefix has been already observed. UNKNOWN in any other case; i.e., the monitor is still uncertain regarding the validity of future trace suffixes. The proposed semantics ensure two key properties of the monitor’s decision procedure. First, the decision procedure is complete – it always produces an output, one of ⊤ , ⊥ or ? . Second, the decision 6.3. Approach Overview 132 procedure is impartial – its outputs are not contradictory over time. Monitors only transition from ? to ⊤ or from ? to ⊥ , never backwards, and never from ⊤ to ⊥ or vice-versa. Unfortunately, another desirable property, soundness cannot be guaranteed. A sound monitor never provides incorrect output. Our monitors, as previously discussed, follow an outline implementation. They are ROS nodes that passively observe the system and the exchanged messages over time. This means that the monitors are subject to the non-deterministic nature of ROS, and it is this non-determinism that puts soundness beyond our reach. To clarify, in Chapter 4, we define the semantics of our specification language in terms of “observing a message on a topic” . For reference: Let 𝕋 be the set of all ROS topics. For all /t ∈ 𝕋 we define a predicate 𝑡 ∈ Psuch that 𝑡(𝑚) is true if and only if a message 𝑚 ∈ 𝕄 can be observed on topic /t. In practice, we know that topics are abstract entities that represent a network connection between two nodes. There is no such thing as a topic entity, where a message is stored, even temporarily. We must build our implementation around one of two related events: either the publication of a message or the reception of a message. Ideally, a smart combination of the two would be used. For example, take the property ‘ globally:/a causes /b within 100 ms ’. If, by analysing the architectural model, we know that the publishers of /b also subscribe to /a , the monitor should track timestamps for the reception of /a and the publication of /b by such nodes. However, figuring out all the best combinations of publication and reception timestamps, for all kinds of system architectures, is far from trivial. In addition, this is an approach that would require instrumentation. Instrumentation enables monitors to observe events as they happened during the execution of a ROS node. There are no out-of-order observations, which is why we previously stated that a grey approach (outline with some instrumentation) was ideal. If instrumentation is not available, we can only refer to the monitor’s reception of a message. And this is where the non-deterministic nature of ROS enters the scene. Under normal circumstances, ROS only guarantees the ordering of messages within the same topic (but even this can be circumvented, e.g., when using UDP as the transport layer). Messages in different topics can be received in a different order from that in which they were published, for various reasons (e.g., network delays, multithreading, etc.). This means that the system could publish, deterministically, within a single thread, a message on /a and then a message on /b . On the other end, the monitor could observe the /b first, and the message on /a afterwards. The same applies to any node in the network, not just the monitors, and, as such, there is nothing we can do regarding this issue. Fortunately, this issue requires such an alignment of factors (timing of the reception of messages, timing of the thread scheduler, etc.) that it should be a relatively rare occurrence in practice. In any case, we advocate that both the system as well as the specified behavioural properties should be designed in such a way that they are resilient to small timing interactions. 6.4. Monitor Implementation 133 Figure 47: Workflow of the proposed Runtime Verification approach. 6.4 Monitor Implementation In the previous section, we have dicussed how the most feasible approach for online monitoring of ROS applications is to synthesize each specified property into a monolithic, standalone ROS monitoring node. The synthesized node is a passive process – it does not interfere with the system’s execution. It should subscribe to each topic the original property refers, and observe the exchanged messages on such topics, until it is able to reach a verdict of either ⊤ or ⊥ . In order to make its verdict easily observable (and usable by other components), the monitoring node should advertise a topic, ~verdict , where the verdict of the monitored property is to be published. If the monitor reaches a verdict of ⊤ (resp. ⊥ ), the monitor should publish a boolean message on ~verdict containing True (resp. False ). At that point, the monitor can safely stop operating – verdicts are final. In every other state, the monitor’s verdict is ? and nothing should be published. The diagram in Figure 47 illustrates the described workflow. Regarding the decision procedure, our monitor implementation is based on automata. More specifically, we implement monitors as state machines whose states and transitions reflect observed messages that are relevant for the property. Naturally, different scopes and property patterns lead to different state machines. In spite of these differences, however, from a high-level point of view, the handling of property scopes changes little from pattern to pattern. Thus, we divide the presentation of our approach by pattern, and discuss scopes where appropriate. Furthermore, binary property patterns (Precedence, Response, Prevention) are quite more complex than unary patterns (Absence, Existence), due to the possible crossreferences between message contents, e.g., ‘ /a as Acauses /b {x = @A.x} ’. If there are no such references, the resulting state machines are much simpler. So, besides the division by pattern, we also subdivide binary patterns into the simple and the general cases. We provide state machine diagrams for each discussed pattern, according to the notation in Figure 48, to help illustrate our approach. All diagrams reflect the implementation for the after-until scope, which 8.5. Summary 236 research with ROS, and the AgRob V16, an agriculture robot, developed as part of a research project, with the aim of becoming a commercial product. In this chapter, we presented the results of these evaluation processes – which, in some cases, have shown near-optimal performance – and discussed the challenges we faced, as well as the limitations of the current approaches. 9 CONCLUSION Robots are here to stay. The world population of service and industrial robots is increasing at a rapid rate, and the Robot Operating System is an established backbone of robotic software development. Initiatives such as the ROSIN EU Horizon 2020 project 1 and the ROS Quality Assurance Working Group 2 are fundamental steps in promoting established software engineering practices, such as Model-driven Engineering. However, despite their efforts, adoption by the general ROS community is still a slow work in progress. Traditional, code-first development processes are the norm, with software models nowhere to be seen. In a fast developing world of robotic software where source code is the major (and, in some cases, the only) artefact one can work with, dependability cases become a useful mechanism to show that a system satisfies a given critical property, using evidence from various analysis techniques. Thus, we set out to answer the following research question. How can existing software analysis techniques (such as Model Checking, Runtime Verification, etc.) and tools be used by non-experts, to improve the quality of ROS applications and to provide the basis for dependability cases? In the final chapter of this dissertation, we restate our thesis and summarise our contributions in this regard. We briefly discuss their practical impact in the community, so far, and opportunities for collaboration that presented themselves along the way. Lastly, we finish by recalling some of the shortcomings of our current approach, and setting out prospects for future work on this topic. 9.1 Summary Over the course of this dissertation, we have provided evidence to support our thesis. Standard software analysis techniques can be employed behind an interface that caters to ROS roboticists. Namely, an interface that (i) takes source code as input, (ii) reverse engineers (formal) models as needed, and that (iii) uses a high-level property specification language that addresses ROS concepts directly. 1https://www.rosin-project.eu/ 2https://discourse.ros.org/c/quality/ 237 9.1. Summary 238 We have discussed a number of approaches to safety property verification in the literature that work well, to an extent, but are not really an answer to our original question. We have seen approaches in Specification-based Testing that target safety properties specified in Linear Temporal Logic [ 12 , 128 ], but neither is this logic expressive enough to capture the full complexity of ROS systems, nor is it a friendly approach for non-experts. A similar situation happens in the domain of Runtime Verification. There are plenty of powerful tools [ 5 , 18 , 51 , 67 , 84 , 85 ], some even working with more expressive logics than LTL, but they present a steep learning curve to non-experts or are simply not capable of verifying certain key properties. On the other end of the spectrum, some authors recognise the need to build architectural models of ROS applications [ 127 , 142 , 156 , 170 ], as we do, in a user-friendly fashion. Their work, however, is limited to publishers and subscribers only, in some cases, and does not build upon the extracted models to check safety properties that address behaviour, rather than structure. Our proposed approach combines the best of both worlds – ease of use by non-experts and verification of complex safety properties – in a single workflow. In this regard, we have made the following contributions: 1. a study on how ROS features are used in practice [149]; 2. a metamodel for ROS applications [151]; 3. an automatic procedure to build models from source code [151]; 4. a specification language to annotate models with behavioural properties [41]; 5. a property-based test generator [150]; 6. the HAROS framework [148] for the analysis of ROS systems. The first contribution is straightforward. It does not have a direct impact towards improving the quality of ROS applications, but it helped us prioritise certain features over others. For instance, our decision to base the property specification language around ROS publishers and subscribers was based on this study. Establishing a metamodel is definitely the first step towards enabling ROS-specific analyses. The ROS community has not proposed an official metamodel, and the benefits of model-based approaches are too good to pass up. At the same time, it allows us to work at a convenient abstraction level of Nodes, Topics and other ROS resources, rather than work only with low-level source code entities. But source code entities are not completely disregarded either. Our metamodel includes such entities, in order to establish a traceability relation between source code entities and ROS computation graph resources. This is a distinguishing feature that we have not seen in other approaches, in spite of its usefulness in terms of lowering maintenance effort – i.e., issues can be traced back to a concrete source code artefact. To complement the proposed metamodel, we put together an automatic model extraction procedure based on static analysis. The choice of static analysis benefits from ease of use and earlier detection, at the cost of increased complexity. In some cases, it might not be able to fully extract all entities. We address this limitation by presenting the incomplete entities up front, and allowing the user to provide the missing pieces of information. On top of these models, we are able to verify a large range of structural properties – e.g., “all Topics have, at most, a single publisher” , or “there is only one Topic for laser scan messages” . More importantly, being a mostly automated process, it is immediately usable by non-experts. 9.2. Impact and Collaborations 239 Our next contribution comes in to address a limitation of the model extraction process, as well as a shortcoming of ROS systems in general: the lack of behaviour properties. While automatic extraction of behaviour properties with static analysis is possible, it requires extensive effort and is, more than likely, very limited in terms of what it can deliver. Instead, we propose a specification language, designed around the exchange of ROS messages. The language is minimalistic, yet capable of expressing many common properties. It is based on Metric First-Order Temporal Logic, in order to be able to capture real-time constraints as well as the full structure of message data. Its formal semantics enable us to reuse state of the art knowledge in property verification, while its syntax masks the details and lowers the barrier to adoption. In addition, this language is based on established specification patterns [ 58 , 59 ] that capture a large portion of use cases. One of its drawbacks, in its current form, is its sole focus on Topics, leaving out Services and Parameters. This was a deliberate decision, given our time constraints. The decision to prioritise Topics over the other primitives was, as mentioned, based on our empirical study. Our penultimate contribution shows one of the many applications of architectural models annotated with behavioural properties. We are able to generate black-box tests that target each of the specified properties, and rely on runtime monitors as oracles. From the architectural models, we know which topics to observe, and what message types are associated with each topic. From the property patterns we build test strategies that attempt to falsify the property. This approach is built on a Property-based Testing tool, that handles input space exploration and minimisation of the counterexamples it finds – yet another major step towards reducing maintenance effort. Our evaluation shows this technique to be effective at finding faults and providing minimal counterexamples – it has even uncovered a previously unknown fault in AgRob V16, a robotic platform for hillside agriculture. Its major drawback is the time it requires to run all generated tests. Piecing together all contributions, as our final contribution, we achieved a workflow that has been fully integrated in the HAROS framework – a ROS-specific analysis tool, initially built as part of the Master’s thesis that preceeded this work, that is progressively gaining traction among the ROS community. 9.2 Impact and Collaborations Our work and our contributions (our technical contributions, in particular) are not purely academic. HAROS and our newly proposed workflow have gathered a fair number of users and supporters, especially in the ROS-Industrial community. They were featured multiple times, in talks and tutorials, in events hosted by the ROS-Industrial Consortium Europe, such as the ROS-Industrial Conference 3 , for instance. HAROS has been used by a small number of companies, and is often used by researchers (both in the domains of Robotics and Software Engineering). It has also been promoted multiple times by the ROS Quality Assurance Working Group as one of the main, readily available tools to analyse ROS systems. More importantly, this line of research has opened up opportunities for a few interesting collaborations that we detail in this section. 3https://rosindustrial.org/events/2016/11/3/2016-ros-industrial-conference https://rosindustrial.org/events/2017/12/12/ros-industrial-conference-2017 https://rosindustrial.org/events/2018/12/11/ros-industrial-conference-2018 9.2. Impact and Collaborations 240 ROBUST – ROS Bug Study We start with our longest-running collaboration effort, with members of the ROSIN European project, that is also the least directly related to this thesis. One of the objectives of the ROSIN project is to raise the overall quality of ROS robotics software. They aim to contribute to this goal by developing code scanners that continuously and automatically analyze ROS software, and detect, as well as report, programming errors and quality issues in the code. In this regard, tools such as HAROS are of great importance to the project. In order to figure out what kind of analysis capabilities are needed – both to extend HAROS and to build other independent tools – we first need to understand what kind of errors ROS developers often make and what kind of code quality issues they often have. To this end, we systematically harvested 266 real documented bugs from a representative collection of ROS code repositories 4 . We then analysed this collection, classified each fault and failure according to a number of categories, and gathered various relevant statistics. The gathered observations will guide the subsequent development of new analysis tools in the ROSIN project. Another goal of this study, besides collecting error reports, is to provide a repository of historically reproducible errors. Analysis and automated repair of historical bugs often requires access to the build and runtime environments in which those bugs were first identified and later fixed. Reproducing such historical environments is challenging, especially with ROS, due to the complex dependencies between ROS versions, tool versions and operating system versions. To accomplish this task, we built a series of tools that aid in tracking down the correct versions. Then, we build Docker 5 images of the environment and ROS application as they were at the time of the error report. In addition, we include test scripts within the reproduction image that show precisely the reported failure. The tests fail for the faulty version of the ROS repository, but pass for the fixed version. The work required to build test scripts for all cases proved to be quite a burden, which turned out to be an additional motivation for our test generator approach. Not all kinds of errors can be captured by our approach, because not all of them are related to software behaviour (e.g., build errors, missing dependencies, etc.), but it can be used to automate in a small number of cases. At the time of writing, this work has only been presented at ROSCon 2019 6 . We are in the process of documenting our findings and preparing a submission to a top Software Engineering journal. Model Extraction for ROS Python Code Our architectural model extraction procedure, as previously stated in Chapter 5, was only implemented for the C ++ ROS client library. C ++ code makes up a large portion of the existing ROS ecosystem, being the go-to choice to implement low-level or performance-critical components, such as drivers and controllers. Python, on the other hand, is a common choice for high-level components, such as planners and orchestrators; components whose performance is not favoured over using an easier programming language. Automated 4https://github.com/robust-rosin/robust 5https://www.docker.com/ 6https://roscon.ros.org/2019/talks/roscon2019_188_bugs_later.pdf https://vimeo.com/378916121 9.2. Impact and Collaborations 241 extraction of models for Python Nodes turned out to be a much-requested feature by HAROS users, and, eventually, it was proposed as a topic for a Master’s thesis. Davide Laezza, a Master’s student of the SQUARE group 7 at the IT University of Copenhagen, under the supervision of professor Andrzej W�sowski – group leader and one of the heads of the ROSIN project – picked up this task and replicated our model extraction approach for the ROS Python client library. Davide defended his thesis in April 2019, and his contribution is now a part of the current HAROS release. Bootstrapping Model-Driven Engineering in ROS Our metamodel for ROS applications, and the respective model extraction procedure, was the catalyst for a second collaborative work, this time with members of the Fraunhofer Institute for Manufacturing Engineering and Automation IPA 8 . The aim of this work is to promote Model-driven Engineering practices in the ROS community. In particular, it shows how modelling can be a complement, rather than an alternative, to manually written code. One way to achieve this is to build system models from existing source code – the same premise that backs our thesis. However, this research initiative does not rely solely on static analysis to build its models. Its first contribution is an approach that merges information gathered at static time with information gathered at runtime. We handled the static analysis model extraction with HAROS, while the runtime part was implemented by members of Fraunhofer IPA. A second contribution is an easy-to-use web infrastructure that performs model extraction using this approach (to alleviate the burden on end users), while, at the same time, building a database of models extracted from various open source projects. The main objective of this tooling, publicly available both as-a-service 9 and as source code 10 , is to lower the MDE barrier for practitioners and leverage models to: • improve the understanding of manually written code; • perform correctness checks; and • systematize the definition and adoption of best practices through large-scale generation of models from existing code. This work, and a case study of its application on Care-O-bot 4 11 (a commercial mobile robot assistant to actively support humans in domestic environments), has been published at the MODELS 2019 conference [ 73 ]. An improved version of this work has been submitted [ 74 ] to the Software and Systems Modeling journal. 7https://square.itu.dk/ 8https://www.ipa.fraunhofer.de/en.html 9http://153.97.4.193/ 10 https://github.com/ipa320/ros-model 11 https://www.care-o-bot.de/en/care-o-bot-4.html 9.3. Prospect for Future Work 242 HAROS Model Checking Plug-in Lastly, Renato Carvalho, a student at our institution, worked on a new plug-in for HAROS as part of his Master’s thesis. This thesis builds on our property specification language, but, rather than building tests, it is used for model checking purposes. Its main goal is to verify system-wide properties in ROS applications, i.e., properties that span a whole Configuration, rather than single Node behaviour. The proposed technique [ 41 ] is based in the formalisation of architectural models and node behaviour in Electrum12 [35], over which system-wide specifications are subsequently model checked. The overall workflow is essentially the same one we propose for automated testing. 1. The user annotates Nodes and Configurations, defined in a HAROS project file, with behavioural properties written in our proposed specification language (Chapter 4). 2. HAROS extracts the system’s architecture, including the Computation Graph. 3. The model checking plug-in uses the system architecture, the user specification and the ROS message definitions to generate a Electrum model. 4. The model checker tries to falsify the model’s assertions. 5. In the case that Electrum finds a counterexample for the property, the counterexample is presented to the user via the HAROS interface. One of the main differences is that, since this approach is based on system-wide properties, node properties are used as axioms of the formalised model, while the system-wide properties are converted to assertions. Another difference is that Electrum is unable to handle real time. The current approach ignores real-time constraints and focuses on finding counterexamples only via classes of values or invalid sequences of messages. This plug-in has been applied not only to the AgRob V16 case sutdy, but also to an internal case study provided by the VORTEX Colab 13 – a Collaborative Laboratory in Cyberphysical Systems and Cybersecurity. This second case study is a ROS prototype for an Advanced Driver-Assistance System. 9.3 Prospect for Future Work We have established a workflow for the analysis and verification of safety properties for ROS applications. The techniques we rely on have some limitations that pose interesting research problems. Furthermore, our approach is not strictly tied to any particular verification technique. Its foundation, based on static analysis and model extraction, provides a great deal of freedom to build on top of. As we have seen, we can verify structural properties on the extracted models themselves, or we can use the models to generate property-based tests, or even to perform model checking. There are a number of other techniques that we can integrate in this workflow. In this section, we discuss some directions for future work that we are likely to explore. 12 http://haslab.github.io/Electrum/ 13 http://www.vortex-colab.com/ 9.3. Prospect for Future Work 243 On Static Analysis and Model Extraction The first step of our proposed workflow is based on static analysis of source code. Without it, we have no access to models, and, thus, are incapable of verifying any properties of the target system. This, of course, depends on the availability of the source code in the first place. While it is often not an issue for systems under development, in many cases ROS developers tend to reuse off-the-shelf components. If such components are installed as binaries, rather than being built from source, they become opaque to our analysis. One of the measures we take to alleviate this problem, is to integrate within HAROS a database of hard-coded models from popular components of the standard ROS distribution. Maintaining such a database, however, is laborious, and is never going to cover all cases, in practice. This limitation is also one of the arguments that is often used in favour of dynamic analyses, rather than static analyses. A massive improvement to this workflow, that would eliminate this initial limitation and make our approach feasible for any ROS system, would be to extend our static analysis techniques to also incorporate binary static analysis , i.e., analysing compiled binaries without executing them. This is based on state of the art techniques from the domain of reverse engineering, and is commonly used for security purposes [24, 94 , 155 , 162 ]. In this case, we would be using it to find calls to the ROS primitives, and reconstruct the architectural model. Powerful reverse engineering tools are freely available, e.g., Radare2 14 , and could be used as a basis for this approach. Binary static analysis could be seen as extending our static analysis capabilities in breadth. On the other hand, we can extend them in depth, using techniques from control flow analysis and data flow analysis. Inspired in previous works for ROS [ 142 , 156 ], we can extend our metamodel to incorporate additional information about a Node’s behaviour. Classifying publishers as proactive, reactive, periodic or rate-independent, we get some insights into the message flow of the system. Moreover, we can explore symbolic execution to determine predicates and properties about published data. This, in turn, would enable us to: • automatically annotate Nodes with behavioural properties, using our specification language; • verify behavioural properties in static time (making, e.g., model checking easier), rather than dynamically. At the level of the models, we can also take various courses of action. One such course is based in the fact that many ROS Configurations are slight variations of one another. We have anecdotally seen this in multiple systems, and we have also mentioned this in Chapter 8of this thesis. TurtleBot2 has numerous instances of very similar configurations, where the difference is in the presence or absence of a single node, such as the safety controller, or keyboard teleoperation, for instance. Even in AgRob V16, many configurations just change initialisation parameters, such as the map to be loaded or the maximum velocity limits. By extracting and comparing models across all configurations, we can find common denominators, build Feature Models and identify Software Product Lines, and their points of variability [ 34 , 118 , 119 , 132 , 173 ]. 14 https://rada.re/n/index.html 9.3. Prospect for Future Work 244 Another course of action is to identify issues in the extracted architecture models – i.e., differences between the designed architecture and the implemented architecture [ 164 ] – and provide suggestions for architecture repair. This can be achieved in various forms, for instance by defining general architectural guidelines [ 115 ] or by using our extraction hint system, with hints being used to repair systems, rather than simply fix the models. Last, but not least, we have proposed in Chapter 3an extension to the metamodel itself, to incorporate high-level concepts provided by libraries, such as Actions and Dynamic Reconfiguration. Granted, these concepts are implemented on top of the basic building blocks of ROS (Topics, Services and Parameters). Even if the metamodel itself is not extended, we can, at least, improve the static analysis step to understand these compound primitives, and convert them into the respective low-level resources. On Property Specification and Verification As we have discussed in Chapter 8, there are a few ways to improve the property specification language itself. The most immediate improvements are the inclusion of event disjunctions, e.g., ‘ /a or /b ’, and the specification of state machines. Other less straightforward enhancements would be the inclusion of other ROS resources, besides Topics, i.e., the inclusion of Services and Parameters. The other resources have fundamentally different mechanics from Topics, which would pose a challenge to specify their semantics. In particular, we anticipate Parameters, which are subject to concurrency and can change at any time without notification, to be the most challenging aspect to formalise. In terms of Runtime Verification, the addition of Services and Parameters would require new monitoring approaches. Topics can be observed by any Node in the network, without restrictions. Services and Parameters, on the other hand, are based on one-to-one connections and cannot be externally observed without interfering with the system. In this regard, we have two main paths that we could follow. 1. Replace the ROS Master node and/or the client libraries with a modified version. Implementing a debug version of the core communication infrastructure of ROS would allow us to inject observers that would monitor Service or Parameter connections. This approach is transparent to the system under test and still allows for treating the system as a black box. 2. Instrument the target system, so that it monitors all calls to Services and Parameters, and relays the events to a central monitor. This approach does not require tampering with the main infrastructure of ROS, but requires building a separate, instrumented version of the target system. It is easier to adopt in a production environment, but it becomes challenging if the system’s source code is not available. In terms of Property-based Testing, as also discussed in Chapter 8, we believe that using simulated time in ROS would be benefitial to uncover hard-to-find timing interactions. However, such carefully crafted scenarios might hardly happen in a real environment, with real time. Furthermore, Nodes are not required to use the ROS-provided clocks, any Node can use real-time clocks instead (thus invalidating the use of simulated time). As such, this technique should be used as a complement, rather than as a substitute for 9.3. Prospect for Future Work 245 the current approach. In addition, counterexamples provided by exploiting simulated time would have to be considered with extra care. The exploited timing interactions might not be possible in a real environment for a multitude of reasons, with the most obvious being performance limitations – e.g., being impossible for a Node to produce multiple large messages within less than one millisecond of one another. Other improvements to the Property-based Testing approach, as suggested in Chapter 7, are mainly concerned with being able to test more properties, and using smarter data generation. Our current approach requires that all topics referenced in a property (except for the behaviour message) be open subscribed topics. As we have discussed, this restriction can be alleviated, making tests more passive and more reliant on runtime monitors. Regarding data generation, we have proposed some best-effort approaches to analyse axioms statically and to automatically refine test schemas; these have not been implemented yet. We have also proposed the use of SMT solvers (Satisfiability Modulo Theories, e.g., Z3 [ 54 ]) or symbolic computing libraries (e.g., SymPy [ 123 ]) to embed arithmetic and quantified expressions directly into Hypothesis strategies. In addition, it is also worth experimenting with custom shrinking approaches to generated input traces, to aim for shorter tests overall. On Technical Improvements Lastly, on a technical side, and covering the whole workflow, our approach can naturally be extended to support ROS2. As more companies and researchers transition to the new version of ROS, for its improved communication infrastructure and real-time capabilities, this feature has been requested multiple times for HAROS. Some of the differences between ROS and ROS2 are minimal. For instance, to extract architectural models from C ++ source code, it requires little more than searching for different function names in the parsed Abstract Syntax Tree. However, other changes have a significant impact in the overall approach, with launch files being a notorious one. The original launch files were deemed to be rather inflexible, despite allowing composition, conditional statements and namespace grouping. In ROS2, launch files were replaced by Python scripts. This change alone greatly diminishes the usefulness of static analysis. It is likely that, in the event that we are not able to fully parse the launch script, we would have to ask the user for parsing hints. Alternatively, we would have to move away from static analysis and run the script itself in a sandbox environment. On a lighter note, ROS2 provides support to implement Nodes that follow a standardised life cycle. This is something that can be leveraged to enhance the extraction of both the system’s architecture as well as the behaviour. Furthermore, it represents an out-of-the-box mechanism to reset a system’s state without shutting it down and bringing it back up, which is one of the major performance obstacles for our Property-based Testing approach, as we have seen in Chapter 8. bibliography 252 [70] D. M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification , pages 409–448, 1989. doi: 10.1007/3-540-51803-7_ 36. [71] D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In ACM Symposium on Principles of Programming Languages (POPL) , pages 163–173, 1980. doi: 10.1145/567446.567462. [72] D. Ganesan, M. Lindvall, L. Ruley, R. Wiegand, V. Ly, and T. Tsui. Architectural analysis of systems based on the publisher-subscriber style. In Working Conference on Reverse Engineering (WCRE) , pages 173–182, 2010. doi: 10.1109/WCRE.2010.27. [73] N. H. Garcia, L. Delval, M. Lüdtke, A. Santos, B. Kahl, and M. Bordignon. Bootstrapping MDE development from ROS manual code - part 2: Model generation. In ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS) , pages 95–105. IEEE, 2019. doi: 10.1109/MODELS.2019.00-11. [74] N. H. Garcia, H. Deshpande, A. Santos, B. Kahl, and M. Bordignon. Bootstrapping MDE development from ROS manual code - part 2: Model generation and leveraging models at runtime. Software and Systems Modeling , 2021 (Accepted). [75] E. Gat. On three-layer architectures. Artificial Intelligence and Mobile Robots , 195:210, 1998. [76] V. Graefe and R. Bischoff. From ancient machines to intelligent robots – a technical evolution. In International Conference on Electronic Measurement & Instruments (ICEMI) , pages 3–418–3–431, 2009. [77] V. Gribov and H. Voos. Safety oriented software engineering process for autonomous robots. In IEEE Conference on Emerging Technologies & Factory Automation (ETFA) , pages 1–8, 2013. doi: 10.1109/ETFA.2013.6647969. [78] R. Halder, J. Proença, N. Macedo, and A. Santos. Formal verification of ROS-based robotic applications using timed-automata. In IEEE/ACM International FME Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE) , pages 44–50, 2017. doi: 10.1109/FormaliSE.2017.9. [79] S. Hallé and R. Villemaire. Runtime monitoring of message-based workflows with data. In International IEEE Enterprise Distributed Object Computing Conference (ECOC) , pages 63–72, Sep. 2008. doi: 10.1109/EDOC.2008.32. [80] S. Hallé and R. Villemaire. Flexible and reliable messaging using runtime monitoring. In IEEE International Enterprise Distributed Object Computing Conference (EDOCw) , pages 116–125, 2009. doi: 10.1109/EDOCW.2009.5332002. bibliography 253 [81] K. Havelund, D. Peled, and D. Ulus. DejaVu: A monitoring tool for first-order temporal logic. In Workshop on Monitoring and Testing of Cyber-Physical Systems (MT@CPSWeek) , pages 12–13, 2018. doi: 10.1109/MT-CPS.2018.00013. [82] C. Heer. Robots double worldwide by 2020. https://ifr.org/ifr-press-releases/ news/robots-double-worldwide-by-2020. [Online; accessed 19-September-2020]. [83] G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering , 23(5): 279–295, 1997. doi: 10.1109/32.588521. [84] C. Hu, W. Dong, Y. Yang, H. Shi, and G. Zhou. Runtime verification on hierarchical properties of ROS-based robot swarms. IEEE Transactions on Reliability , pages 1–16, 2019. doi: 10.1109/TR. 2019.2923681. [85] J. Huang, C. Erdogan, Y. Zhang, B. M. Moore, Q. Luo, A. Sundaresan, and G. Rosu. ROSRV: runtime verification for robots. In International Conference on Runtime Verification (RV) , pages 247–254, 2014. doi: 10.1007/978-3-319-11164-3_20. [86] J. Hughes. Experiences with quickcheck: Testing the hard stuff and staying sane. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday , pages 169–186, 2016. doi: 10.1007/978-3-319-30936-1_9. [87] IFR. Mobile robot transports sterile goods in hospital. https://ifr.org/ ifr-press-releases/news/mobile-robot-transports-sterile-goods-in-hospital , . [Online; accessed 19-September-2020]. [88] IFR. Battling the coronavirus with uv lighting. https://ifr.org/ifr-press-releases/ news/battling-the-coronavirus-with-uv-lighting , . [Online; accessed 19September-2020]. [89] D. Jackson. A direct path to dependable software. Communications of the ACM , 52(4):78–88, 2009. doi: 10.1145/1498765.1498787. [90] D. Jackson and C. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. In International Symposium on Software Testing and Analysis (ISSTA) , pages 239–249, 1996. doi: 10.1145/229000.226322. [91] Y. Jiang, S. Hou, J. Shan, L. Zhang, and B. Xie. An approach to testing black-box components using contract-based mutation. International Journal of Software Engineering and Knowledge Engineering , 18(1):93–117, 2008. doi: 10.1142/S0218194008003556. [92] A. Kane, O. Chowdhury, A. Datta, and P. Koopman. A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In International Conference on Runtime Verification (RV) , pages 102–117. Springer International Publishing, 2015. ISBN 978-3-319-23820-3. doi: 10.1007/978-3-319-23820-3_7. bibliography 254 [93] G. Kanter and J. Vain. TestIt: an open-source scalable long-term autonomy testing toolkit for ROS. In International Conference on Dependable Systems, Services and Technologies (DESSERT) , pages 45–50, 2019. doi: 10.1109/DESSERT.2019.8770011. [94] N. Karampatziakis. Static analysis of binary executables using structural svms. In Advances in Neural Information Processing Systems 23 , pages 1063–1071. Curran Associates, Inc., 2010. [95] R. M. Karp. An algorithm to solve the m × n assignment problem in expected time O ( mn log n ). Networks , 10(2):143–152, 1980. doi: 10.1002/net.3230100205. [96] A. Khalili, L. Natale, and A. Tacchella. Reverse engineering of middleware for verification of robot control architectures. In International Conference on Simulation, Modeling, and Programming for Autonomous Robots (SIMPAR) , pages 315–326, 2014. doi: 10.1007/978-3-319-11900-7_27. [97] R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems , 2(4): 255–299, 1990. doi: 10.1007/BF01995674. [98] K. Krogmann. Reconstruction of Software Component Architectures and Behaviour Models Using Static and Dynamic Analysis . PhD thesis, Karlsruhe Institute of Technology, Germany, 2010. [99] P. S. Kumar, W. Emfinger, A. Kulkarni, G. Karsai, D. Watkins, B. Gasser, C. Ridgewell, and A. Anilkumar. ROSMOD: a toolsuite for modeling, generating, deploying, and managing distributed real-time component-based software using ROS. In International Symposium on Rapid System Prototyping (RSP) , pages 39–45, 2015. doi: 10.1109/RSP.2015.7416545. [100] L. Lamport, J. Matthews, M. R. Tuttle, and Y. Yu. Specifying and verifying systems with TLA+. In ACM SIGOPS European Workshop , pages 45–48. ACM, 2002. doi: 10.1145/1133373.1133382. [101] L. Lampropoulos, M. Hicks, and B. C. Pierce. Coverage guided, property based testing. ACM on Programming Languages , 3(OOPSLA):181:1–181:29, 2019. doi: 10.1145/3360607. [102] R. Larrieu and N. Shankar. A framework for high-assurance quasi-synchronous systems. In ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) , pages 72–83, 2014. doi: 10.1109/MEMCOD.2014.6961845. [103] M. Larsen, M. Adam, U. Schultz, and R. Jørgensen. Towards Automatic Consistency Checking of Software Components in Field Robotics , pages 409–418. 2014. ISBN 978-84-697-0248-2. [104] T. Latvala, A. Biere, K. Heljanko, and T. A. Junttila. Simple bounded LTL model checking. In International Conference on Formal Methods in Computer-Aided Design (FMCAD) , pages 186–200, 2004. doi: 10.1007/978-3-540-30494-4_14. [105] C. Lesire, D. Doose, and H. Cassé. Mauve: a component-based modeling framework for real-time analysis of robotic applications. In Workshop on Software Development and Integrationin Robotics (SDIR-VII ICRA) , 2012. bibliography 255 [106] C. Lesire, S. Roussel, D. Doose, and C. Grand. Synthesis of real-time observers from past-time linear temporal logic and timed specification. In International Conference on Robotics and Automation (ICRA) , pages 597–603, 2019. doi: 10.1109/ICRA.2019.8793754. [107] W. Li, L. Gérard, and N. Shankar. Design and verification of multi-rate distributed systems. In ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) , pages 20–29, 2015. doi: 10.1109/MEMCOD.2015.7340463. [108] X. Li, R. Wang, Y. Jiang, Y. Guan, X. Li, and X. Song. Formal modeling and automatic code synthesis for robot system. In International Conference on Engineering of Complex Computer Systems (ICECCS) , pages 146–149, 2017. doi: 10.1109/ICECCS.2017.17. [109] A. Löscher and K. Sagonas. Targeted property-based testing. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , pages 46–56. ACM, 2017. doi: 10.1145/ 3092703.3092711. [110] A. Löscher and K. Sagonas. Automating targeted property-based testing. In IEEE International Conference on Software Testing, Verification and Validation (ICST) , pages 70–80, 2018. doi: 10.1109/ICST.2018.00017. [111] A. Löscher, K. Sagonas, and T. Voigt. Property-based testing of sensor networks. In IEEE International Conference on Sensing, Communication, and Networking (SECON) , pages 100–108, 2015. doi: 10.1109/SAHCN.2015.7338296. [112] D. MacIver, Z. Hatfield-Dodds, and M. Contributors. Hypothesis: A new approach to propertybased testing. Journal of Open Source Software , 4(43):1891, 11 2019. ISSN 2475-9066. doi: 10.21105/joss.01891. [113] D. R. MacIver. What is property based testing? https://hypothesis.works/articles/ what-is-property-based-testing/. [Online; accessed 30-November-2020]. [114] D. R. MacIver. Hypothesis 5.6.0. https://github.com/HypothesisWorks/hypothesis, 2020. [115] I. Malavolta, G. Lewis, B. Schmerl, P. Lago, and D. Garlan. How do you architect your robots? state of the practice and guidelines for ros-based systems. ICSE-CEIP. ACM , 10(3377813.3381358), 2020. [116] Z. Manna and A. Pnueli. Verification of concurrent programs, part I: The temporal framework. In The Correctness Problem in Computer Science , pages 215–273, 1981. [117] N. Markey. Temporal logic with past is exponentially more succinct. Bulletin of the EATCS , 79: 122–128, 2003. bibliography 256 [118] J. Martinez, T. Ziadi, T. F. Bissyandé, J. Klein, and Y. L. Traon. Automating the extraction of model-based software product lines from model variants (T). In IEEE/ACM International Conference on Automated Software Engineering (ASE) , pages 396–406. IEEE Computer Society, 2015. doi: 10.1109/ASE.2015.44. [119] J. Martinez, X. Tërnava, and T. Ziadi. Software product line extraction from variability-rich systems: The robocode case study. In International Systems and Software Product Line Conference - Volume 1 (SPLC) , pages 132–142. ACM, 2018. doi: 10.1145/3233027.3233038. [120] B. Mayer and R. Weinreich. An approach to extract the architecture of microservice-based software systems. In IEEE Symposium on Service-Oriented System Engineering (SOSE) , pages 21–30, 2018. doi: 10.1109/SOSE.2018.00012. [121] W. Meng, J. Park, O. Sokolsky, S. Weirich, and I. Lee. Verified ROS-based deployment of platformindependent control systems. In NASA Formal Methods (NFM) , pages 248–262, 2015. doi: 10.1007/978-3-319-17524-9_18. [122] G. Metta, P. Fitzpatrick, and L. Natale. YARP: Yet Another Robot Platform. International Journal of Advanced Robotic Systems , 3(1):8, 2006. doi: 10.5772/5761. [123] A. Meurer, C. P. Smith, M. Paprocki, O. Certík, S. B. Kirpichev, M. Rocklin, A. Kumar, S. Ivanov, J. K. Moore, S. Singh, T. Rathnayake, S. Vig, B. E. Granger, R. P. Muller, F. Bonazzi, H. Gupta, S. Vats, F. Johansson, F. Pedregosa, M. J. Curry, A. R. Terrel, S. Roucka, A. Saboo, I. Fernando, S. Kulal, R. Cimrman, and A. M. Scopatz. SymPy: symbolic computing in Python. PeerJ Computer Science , 3:e103, 2017. doi: 10.7717/peerj-cs.103. [124] M. Micallef and C. Colombo. Lessons learnt from using DSLs for automated software testing. In IEEE International Conference on Software Testing, Verification and Validation (ICST) , pages 1–6, 2015. doi: 10.1109/ICSTW.2015.7107472. [125] A. Michlmayr, P. Fenkam, and S. Dustdar. Specification-based unit testing of publish/subscribe applications. In International Conference on Distributed Computing Systems Workshops (ICDCS) , page 34, 2006. doi: 10.1109/ICDCSW.2006.103. [126] M. Mostafa and B. Bonakdarpour. Decentralized runtime verification of LTL specifications in distributed systems. In IEEE International Parallel and Distributed Processing Symposium (IPDPS) , pages 494–503, 2015. doi: 10.1109/IPDPS.2015.95. [127] B. J. Muscedere, R. Hackman, D. Anbarnam, J. M. Atlee, I. J. Davis, and M. W. Godfrey. Detecting feature-interaction symptoms in automotive software using lightweight analysis. In IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER) , pages 175–185, 2019. doi: 10.1109/SANER.2019.8668042. bibliography 257 [128] M. Narizzano, L. Pulina, A. Tacchella, and S. Vuotto. Automated requirements-based testing of black-box reactive systems. In NASA Formal Methods (NFM) , volume 12229 of Lecture Notes in Computer Science , pages 153–169. Springer, 2020. doi: 10.1007/978-3-030-55754-6_9. [129] J. P. Near, A. Milicevic, E. Kang, and D. Jackson. A lightweight code analysis and its role in evaluation of a dependability case. In International Conference on Software Engineering (ICSE) , pages 31–40. ACM, 2011. doi: 10.1145/1985793.1985799. [130] N. J. Nilsson. Principles of Artificial Intelligence . Morgan Kaufmann Publishers Inc., 1980. ISBN 0934613109. [131] V. Okun. Specification Mutation For Test Generation And Analysis . PhD thesis, University of Maryland, Baltimore County, 2004. [132] P. Oliveira, G. Vale, P. A. Júnior, and H. Costa. Extraction of a software product line using conditional compilation - an exploratory study. In Latin American Computing Conference (CLEI) , pages 1–10. IEEE, 2019. doi: 10.1109/CLEI47609.2019.9089045. [133] J. Ore, C. Detweiler, and S. G. Elbaum. Lightweight detection of physical unit inconsistencies without program annotations. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , pages 341–351, 2017. doi: 10.1145/3092703.3092722. [134] J. Ore, C. Detweiler, and S. G. Elbaum. Phriky-units: A lightweight, annotation-free physical unit inconsistency detection tool. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , pages 352–355, 2017. doi: 10.1145/3092703.3098219. [135] J. Ore, S. G. Elbaum, and C. Detweiler. Dimensional inconsistencies in code and ROS messages: A study of 5.9M lines of code. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , pages 712–718, 2017. doi: 10.1109/IROS.2017.8202229. [136] D. L. Parnas, A. J. van Schouwen, and S. P. Kwan. Evaluation of safety-critical software. Communications of the ACM , 33(6):636–648, 1990. doi: 10.1145/78973.78974. [137] S. Pearson. The digital and electronic revolution: Some important milestones. http://www. thepeoplehistory.com/electronics.html. [Online; accessed 19-September-2020]. [138] I. Perez and H. Nilsson. Testing and debugging functional reactive programming. PACMPL , 1(ICFP): 2:1–2:27, 2017. doi: 10.1145/3110246. [139] M. Pichler, B. Dieber, and M. Pinzger. Can I depend on you? mapping the dependency and quality landscape of ROS packages. In IEEE International Conference on Robotic Computing (IRC) , pages 78–85, 2019. doi: 10.1109/IRC.2019.00020. [140] A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science , pages 46–57, 1977. doi: 10.1109/SFCS.1977.32. bibliography 258 [141] A. Pretschner, W. Prenninger, S. Wagner, C. Kühnel, M. Baumgartner, B. Sostawa, R. Zölch, and T. Stauner. One evaluation of model-based testing and its automation. CoRR , abs/1701.06815, 2017. [142] R. Purandare, J. Darsie, S. G. Elbaum, and M. B. Dwyer. Extracting conditional component dependence for distributed robotic systems. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , pages 1533–1540, 2012. doi: 10.1109/IROS.2012.6385719. [143] M. Quigley, K. Conley, B. P. Gerkey, J. Faust, T. Foote, J. Leibs, R. Wheeler, and A. Y. Ng. ROS: An open-source Robot Operating System. In ICRA Workshop on Open Source Software , 2009. URL https://www.willowgarage.com/sites/default/files/icraoss09-ROS.pdf. [144] L. Ramasubramanian. The digital revolution. In Geographic Information Science and Public Participation , Advances in Geographic Information Science, pages 19–32. Springer, 2008. ISBN 978-3-540-75400-8. [145] N. Rapin. ARTiMon monitoring tool, the time domains. In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES) , pages 106–122, 2017. [146] J. Raskin and P. Schobbens. State clock logic: A decidable real-time logic. In International Workshop on Hybrid and Real-Time Systems (HART) , pages 33–47, 1997. doi: 10.1007/BFb0014711. [147] C. Riva and J. V. Rodríguez. Combining static and dynamic views for architecture reconstruction. In European Conference on Software Maintenance and Reengineering (CSMR) , page 47, 2002. doi: 10.1109/CSMR.2002.995789. [148] A. Santos, A. Cunha, N. Macedo, and C. Lourenço. A framework for quality assessment of ROS repositories. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , pages 4491–4496, 2016. doi: 10.1109/IROS.2016.7759661. [149] A. Santos, A. Cunha, N. Macedo, R. Arrais, and F. N. dos Santos. Mining the usage patterns of ROS primitives. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , pages 3855–3860, 2017. doi: 10.1109/IROS.2017.8206237. [150] A. Santos, A. Cunha, and N. Macedo. Property-based testing for the robot operating system. In ACM SIGSOFT International Workshop on Automating Test Case Design, Selection, and Evaluation (A-TEST@ESEC/SIGSOFT FSE) , pages 56–62, 2018. doi: 10.1145/3278186.3278195. [151] A. Santos, A. Cunha, and N. Macedo. Static-time extraction and analysis of the ROS computation graph. In IEEE International Conference on Robotic Computing (IRC) , pages 62–69, 2019. doi: 10.1109/IRC.2019.00018. bibliography 259 [152] L. Santos, F. N. dos Santos, S. Magalhães, P. Costa, and R. Reis. Path planning approach with the extraction of topological maps from occupancy grid maps in steep slope vineyards. In IEEE International Conference on Autonomous Robot Systems and Competitions (ICARSC) , pages 1–7. IEEE, 2019. doi: 10.1109/ICARSC.2019.8733630. [153] J. Schumann, P. Moosbrugger, and K. Y. Rozier. R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In International Conference on Runtime Verification (RV) , pages 233–249, 2015. doi: 10.1007/978-3-319-23820-3_15. [154] I. Segura-Bedmar, P. Martínez, and M. Herrero-Zazo. SemEval-2013 task 9 : Extraction of drug-drug interactions from biomedical texts (ddiextraction 2013). In International Workshop on Semantic Evaluation (SemEval@NAACL-HLT) , pages 341–350, 2013. [155] A. Sepp, B. Mihaila, and A. Simon. Precise static analysis of binaries by extracting relational information. In Working Conference on Reverse Engineering (WCRE) , pages 357–366. IEEE Computer Society, 2011. doi: 10.1109/WCRE.2011.50. [156] N. Sharma, S. G. Elbaum, and C. Detweiler. Rate impact analysis in robotic systems. In IEEE International Conference on Robotics and Automation (ICRA) , pages 2089–2096, 2017. doi: 10.1109/ICRA.2017.7989240. [157] C. E. Silva and J. C. Campos. Combining static and dynamic analysis for the reverse engineering of web applications. In ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS) , pages 107–112, 2013. [158] M. Sokolova, N. Japkowicz, and S. Szpakowicz. Beyond accuracy, f-score and ROC: A family of discriminant measures for performance evaluation. In Advances in Artificial Intelligence (AI) , volume 4304 of Lecture Notes in Computer Science , pages 1015–1021. Springer, 2006. doi: 10.1007/11941439_114. [159] T. J. Sørensen. A method of establishing groups of equal amplitude in plant sociology based on similarity of species content and its application to analyses of the vegetation on Danish commons. Det Kongelige Danske Videnskabernes Selskab , 5(4):1–34, 1948. [160] D. Stampfer, A. Lotz, M. Lutz, and C. Schlegel. The SmartMDSD toolchain: An integrated MDSD workflow and integrated development environment (IDE) for robotics software. Journal of Software Engineering for Robotics (JOSER) , 7:3–19, 08 2016. [161] L. Tan, O. Sokolsky, and I. Lee. Specification-based testing with linear temporal logic. In IEEE International Conference on Information Reuse and Integration (IRI) , pages 493–498, 2004. doi: 10.1109/IRI.2004.1431509. bibliography 260 [162] H. Theiling. Extracting safe and precise control flow from binaries. In International Workshop on Real-Time Computing and Applications Symposium (RTCSA) , pages 23–30. IEEE Computer Society, 2000. doi: 10.1109/RTCSA.2000.896367. [163] M. S. A. Trab, S. Counsell, and R. M. Hierons. Specification mutation analysis for validating timed testing approaches based on timed automata. In IEEE Computer Software and Applications Conference (COMPSAC) , pages 660–669, 2012. doi: 10.1109/COMPSAC.2012.93. [164] J. B. Tran and R. C. Holt. Forward and reverse repair of software architecture. In Conference of the Centre for Advanced Studies on Collaborative Research , page 12. IBM, 1999. [165] M. Y. Vardi. Branching vs. linear time: Final showdown. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , pages 1–22, 2001. doi: 10.1007/3-540-45319-9_1. [166] L. Villalobos-Arias, C. Quesada-López, A. Martínez, and M. Jenkins. Evaluation of a model-based testing platform for Java applications. IET Software , 14(2):115–128, 2020. doi: 10.1049/iet-sen. 2019.0036. [167] M. Webster, C. Dixon, M. Fisher, M. Salem, J. Saunders, K. L. Koay, and K. Dautenhahn. Formal verification of an autonomous personal robotic assistant. In AAAI Spring Symposia , 2014. [168] M. Webster, C. Dixon, M. Fisher, M. Salem, J. Saunders, K. L. Koay, K. Dautenhahn, and J. SaezPons. Toward reliable autonomous robotic assistants through formal verification: A case study. IEEE Transactions on Human-Machine Systems , 46(2):186–196, 2016. doi: 10.1109/THMS.2015. 2425139. [169] M. Wenger, W. Eisenmenger, G. Neugschwandtner, B. Schneider, and A. Zoitl. A model based engineering tool for ROS component compositioning, configuration and generation of deployment information. In IEEE International Conference on Emerging Technologies and Factory Automation (ETFA) , pages 1–8, 2016. doi: 10.1109/ETFA.2016.7733559. [170] T. Witte and M. Tichy. Checking consistency of robot software architectures in ROS. In IEEE/ACM International Workshop on Robotics Software Engineering (RoSE) , pages 1–8, 2018. doi: 10.1145/ 3196558.3196559. [171] S. Zaman, G. Steinbauer, J. Maurer, P. Lepej, and S. Uran. An integrated model-based diagnosis and repair architecture for ROS-based robot systems. In IEEE International Conference on Robotics and Automation (ICRA) , pages 482–489, 2013. doi: 10.1109/ICRA.2013.6630618. [172] S. Zander, G. Heppner, G. Neugschwandtner, R. Awad, M. Essinger, and N. Ahmed. A model-driven engineering approach for ROS using ontological semantics. CoRR , abs/1601.03998, 2016. bibliography 261 [173] B. Zhang and M. Becker. Code-based variability model extraction for software product line improvement. In International Software Product Line Conference (SPLC) , pages 91–98. ACM, 2012. doi: 10.1145/2364412.2364428. A.1. Fictibot Driver Package 268 1#include <cstdlib> 2#include <std_msgs/Int8.h> 3#include "fictibot_drivers/sensor_manager.h" 4 5SensorManager::SensorManager(ros::NodeHandle& n, double hz) { 6uint32_t queue_size = (uint32_t) hz * 2 + 1; 7bumper_publisher_ = n.advertise<std_msgs::Int8>("bumper", queue_size); 8laser_publisher_ = n.advertise<std_msgs::Int8>("laser", queue_size); 9wheel_drop_publisher_ = n.advertise<std_msgs::Int8>("wheel", queue_size); 10 } 11 12 void SensorManager::spin() { 13 std_msgs::Int8 bumper_msg; 14 bumper_msg.data = read_bumper(); 15 bumper_publisher_.publish(bumper_msg); 16 std_msgs::Int8 laser_msg; 17 laser_msg.data = read_laser(); 18 laser_publisher_.publish(laser_msg); 19 std_msgs::Int8 wheel_msg; 20 wheel_msg.data = read_wheels(); 21 wheel_drop_publisher_.publish(wheel_msg); 22 } 23 24 int8_t SensorManager::read_bumper() { 25 // left[0,1] | center[0,1] | right[0,1] 26 return (int8_t) (std::rand() % 8); 27 } 28 29 int8_t SensorManager::read_laser() { 30 return (int8_t) (std::rand() % 128); 31 } 32 33 int8_t SensorManager::read_wheels() { 34 // left[0,3] | right[0,3] 35 return (int8_t) (std::rand() % 16); 36 } Listing A.7: The src/sensor_manager.cpp file. A.2. Fictibot Controller Package 269 1#include <ros/ros.h> 2#include "fictibot_drivers/sensor_manager.h" 3#include "fictibot_drivers/motor_manager.h" 4 5int main(int argc, char **argv) { 6ros::init(argc, argv, "fictibot_driver"); 7ros::NodeHandle n; 8SensorManager sensor_man(n, 10 /*Hz*/); 9MotorManager motor_man(n, 10 /*Hz*/); 10 ros::Rate loop_rate(10 /*Hz*/); 11 while (ros::ok()) { 12 sensor_man.spin(); 13 motor_man.spin(); 14 loop_rate.sleep(); 15 } 16 return 0; 17 } Listing A.8: The src/driver_node.cpp file. a.2 Fictibot Controller Package Figure 89: The fictibot_controller package tree. A.2. Fictibot Controller Package 270 1<?xml version="1.0"?> 2<package> 3<name>fictibot_controller</name> 4<version>0.1.0</version> 5<description>The fictibot_controller package</description> 6 7<maintainer email="[email protected]">Andre Santos</maintainer> 8<license>MIT</license> 9<author email="[email protected]">Andre Santos</author> 10 11 <buildtool_depend>catkin</buildtool_depend> 12 <build_depend>roscpp</build_depend> 13 <build_depend>std_msgs</build_depend> 14 <build_depend>fictibot_msgs</build_depend> 15 <run_depend>roscpp</run_depend> 16 <run_depend>std_msgs</run_depend> 17 <run_depend>fictibot_msgs</run_depend> 18 <run_depend>fictibot_drivers</run_depend> 19 </package> Listing A.9: The package.xml file. 1cmake_minimum_required(VERSION 2.8.3) 2project(fictibot_controller) 3 4find_package(catkin REQUIRED COMPONENTS roscpp std_msgs fictibot_msgs) 5catkin_package(INCLUDE_DIRS include CATKIN_DEPENDS roscpp std_msgs fictibot_msgs) 6include_directories(include ${catkin_INCLUDE_DIRS}) 7 8add_executable(fictibot_controller 9src/controller_node.cpp 10 src/random_controller.cpp 11 ) 12 13 add_dependencies(fictibot_controller 14 ${${PROJECT_NAME}_EXPORTED_TARGETS} 15 ${catkin_EXPORTED_TARGETS} 16 ) 17 18 target_link_libraries(fictibot_controller ${catkin_LIBRARIES}) Listing A.10: The CMakeLists.txt file. A.2. Fictibot Controller Package 271 1#ifndef RANDOM_CONTROLLER_H_ 2#define RANDOM_CONTROLLER_H_ 3 4#include <ros/ros.h> 5#include <std_msgs/Int8.h> 6#include <fictibot_msgs/Custom.h> 7 8class RandomController { 9public: 10 RandomController(ros::NodeHandle& n, double hz); 11 ~RandomController(){}; 12 void spin(); 13 private: 14 bool stop_; 15 bool laser_proximity_; 16 bool bumper_left_pressed_; 17 bool bumper_center_pressed_; 18 bool bumper_right_pressed_; 19 bool wheel_left_dropped_; 20 bool wheel_right_dropped_; 21 double stop_cycles_, stop_counter_; 22 ros::Publisher stop_publisher_, command_publisher_; 23 ros::Subscriber laser_subscriber_, bumper_subscriber_, 24 wheel_drop_subscriber_, custom_subscriber_; 25 26 void laser_callback(const std_msgs::Int8::ConstPtr& msg); 27 void bumper_callback(const std_msgs::Int8::ConstPtr& msg); 28 void wheel_callback(const std_msgs::Int8::ConstPtr& msg); 29 void custom_callback(const fictibot_msgs::Custom::ConstPtr& msg); 30 }; 31 32 #endif /*RANDOM_CONTROLLER_H_*/ Listing A.11: The include/fictibot_controller/random_controller.h file. A.2. Fictibot Controller Package 272 1#define _USE_MATH_DEFINES 2 3#include <math.h> 4#include <cstdlib> 5#include <std_msgs/Empty.h> 6#include <std_msgs/Float64.h> 7#include "fictibot_controller/random_controller.h" 8 9RandomController::RandomController(ros::NodeHandle& n, double hz) 10 : stop_(false) 11 , laser_proximity_(false) 12 , bumper_left_pressed_(false) 13 , bumper_center_pressed_(false) 14 , bumper_right_pressed_(false) 15 , wheel_left_dropped_(false) 16 , wheel_right_dropped_(false) 17 , stop_counter_(0) { 18 stop_cycles_ = 2 * hz + 1; 19 uint32_t queue_size = (uint32_t) hz * 2 + 1; 20 std::string some_param; 21 n.param<std::string>("param", some_param, "nothing"); 22 n.setParam("set_param", some_param); 23 command_publisher_ = n.advertise<std_msgs::Float64>("controller_cmd", 1); 24 stop_publisher_ = n.advertise<std_msgs::Empty>("/stop_cmd", 0); 25 laser_subscriber_ = n.subscribe("laser", queue_size, 26 &RandomController::laser_callback, this); 27 bumper_subscriber_ = n.subscribe("bumper", queue_size, 28 &RandomController::bumper_callback, this); 29 wheel_drop_subscriber_ = n.subscribe("wheel", queue_size, 30 &RandomController::wheel_callback, this); 31 if (some_param == "nothing") { 32 custom_subscriber_ = n.subscribe("custom_noparam", queue_size, 33 &RandomController::custom_callback, this); 34 }else { 35 custom_subscriber_ = n.subscribe("custom_w_param", queue_size, 36 &RandomController::custom_callback, this); 37 } 38 } 39 40 void RandomController::laser_callback(const std_msgs::Int8::ConstPtr& msg) { 41 laser_proximity_ = msg->data <= 50; 42 } 43 44 void RandomController::custom_callback( 45 const fictibot_msgs::Custom::ConstPtr& msg) { 46 ROS_INFO("Received custom message!"); 47 } Listing A.12: The src/random_controller.cpp file (part 1 of 2). A.2. Fictibot Controller Package 273 1void RandomController::spin() { 2ros::spinOnce(); 3bool prev_stop = stop_; 4stop_counter_--; 5stop_ = laser_proximity_ || bumper_left_pressed_ || bumper_center_pressed_ 6|| bumper_right_pressed_ || wheel_left_dropped_ || wheel_right_dropped_; 7if (!prev_stop && stop_) { 8std_msgs::Empty stop_msg; 9stop_publisher_.publish(stop_msg); 10 stop_counter_ = stop_cycles_; 11 std_msgs::Float64 vel_msg; 12 vel_msg.data = (double) (std::rand() % 360 - 180) * M_PI / 180.0; 13 command_publisher_.publish(vel_msg); 14 } 15 if (stop_ && stop_counter_ < 0) { 16 stop_counter_ = stop_cycles_; 17 std_msgs::Float64 vel_msg; 18 vel_msg.data = (double) (std::rand() % 360 - 180) * M_PI / 180.0; 19 command_publisher_.publish(vel_msg); 20 } 21 } 22 23 void RandomController::bumper_callback(const std_msgs::Int8::ConstPtr& msg) { 24 int left = msg->data & 4; 25 int center = msg->data & 2; 26 int right = msg->data & 1; 27 if (left) { bumper_left_pressed_ = true; } 28 else { bumper_left_pressed_ = false; } 29 if (center) { bumper_center_pressed_ = true; } 30 else { bumper_center_pressed_ = false; } 31 if (right) { bumper_right_pressed_ = true; } 32 else { bumper_right_pressed_ = false; } 33 } 34 35 void RandomController::wheel_callback(const std_msgs::Int8::ConstPtr& msg) { 36 int left = msg->data & 12; 37 int right = msg->data & 3; 38 if (left == 3) { wheel_left_dropped_ = true; } 39 else if (left == 2 && right >= 1) { wheel_left_dropped_ = true; } 40 else if (left < 2) { wheel_left_dropped_ = false; } 41 if (right == 3) { wheel_right_dropped_ = true; } 42 else if (right == 2 && left >= 1) { wheel_right_dropped_ = true; } 43 else if (right < 2) { wheel_right_dropped_ = false; } 44 } Listing A.13: The src/random_controller.cpp file (part 2 of 2). A.3. Fictibot Multiplexer Package 274 1#include <ros/ros.h> 2#include "fictibot_controller/random_controller.h" 3 4int main(int argc, char **argv) { 5ros::init(argc, argv, "fictibot_controller"); 6ros::NodeHandle n; 7RandomController controller(n, 10 /*Hz*/); 8ros::Rate loop_rate(10 /*Hz*/); 9while (ros::ok()) { 10 controller.spin(); 11 loop_rate.sleep(); 12 } 13 return 0; 14 } Listing A.14: The src/controller_node.cpp file. 1<launch> 2<node name="fictibase" pkg="fictibot_drivers" type="fictibot_driver" /> 3<node name="ficticontrol" pkg="fictibot_controller" type="fictibot_controller" /> 4</launch> Listing A.15: The launch/minimal.launch file. 1<launch> 2<node name="fictibase" pkg="fictibot_drivers" type="fictibot_driver" /> 3<node name="fictiplex" pkg="fictibot_multiplex" type="fictibot_multiplex" /> 4<node name="ficticontrol" pkg="fictibot_controller" type="fictibot_controller"> 5<remap from="controller_cmd" to="normal_priority_cmd" /> 6<remap from="/stop_cmd" to="normal_priority_stop" /> 7</node> 8</launch> Listing A.16: The launch/multiplexer.launch file. a.3 Fictibot Multiplexer Package Figure 90: The fictibot_multiplex package tree. A.3. Fictibot Multiplexer Package 275 1<?xml version="1.0"?> 2<package> 3<name>fictibot_multiplex</name> 4<version>0.1.0</version> 5<description>The fictibot_multiplex package</description> 6 7<maintainer email="[email protected]">Andre Santos</maintainer> 8<license>MIT</license> 9<author email="[email protected]">Andre Santos</author> 10 11 <buildtool_depend>catkin</buildtool_depend> 12 <build_depend>roscpp</build_depend> 13 <build_depend>std_msgs</build_depend> 14 <run_depend>roscpp</run_depend> 15 <run_depend>std_msgs</run_depend> 16 <run_depend>fictibot_drivers</run_depend> 17 </package> Listing A.17: The package.xml file. 1cmake_minimum_required(VERSION 2.8.3) 2project(fictibot_multiplex) 3 4find_package(catkin REQUIRED COMPONENTS roscpp std_msgs) 5catkin_package(INCLUDE_DIRS include CATKIN_DEPENDS roscpp std_msgs) 6include_directories(include ${catkin_INCLUDE_DIRS}) 7 8add_executable(fictibot_multiplex 9src/multiplex_node.cpp 10 src/trichannel_multiplex.cpp 11 ) 12 13 add_dependencies(fictibot_multiplex 14 ${${PROJECT_NAME}_EXPORTED_TARGETS} 15 ${catkin_EXPORTED_TARGETS} 16 ) 17 18 target_link_libraries(fictibot_multiplex ${catkin_LIBRARIES}) Listing A.18: The CMakeLists.txt file. A.3. Fictibot Multiplexer Package 276 1#ifndef TRICHANNEL_MULTIPLEX_HPP_ 2#define TRICHANNEL_MULTIPLEX_HPP_ 3 4#include <ros/ros.h> 5#include <std_msgs/Empty.h> 6#include <std_msgs/Int8.h> 7#include <std_msgs/Float64.h> 8 9class TriChannelMultiplexer { 10 public: 11 TriChannelMultiplexer(ros::NodeHandle& n, double hz); 12 ~TriChannelMultiplexer(){}; 13 void spin(); 14 private: 15 int channel_, priority_cycles_, inactivity_counter_; 16 ros::Publisher stop_publisher_, command_publisher_, state_publisher_; 17 ros::Subscriber high_cmd_subscriber_, high_stop_subscriber_, 18 normal_cmd_subscriber_, normal_stop_subscriber_, 19 low_cmd_subscriber_, low_stop_subscriber_; 20 21 void high_cmd_callback(const std_msgs::Float64::ConstPtr& msg); 22 void high_stop_callback(const std_msgs::Empty::ConstPtr& msg); 23 void normal_cmd_callback(const std_msgs::Float64::ConstPtr& msg); 24 void normal_stop_callback(const std_msgs::Empty::ConstPtr& msg); 25 void low_cmd_callback(const std_msgs::Float64::ConstPtr& msg); 26 void low_stop_callback(const std_msgs::Empty::ConstPtr& msg); 27 }; 28 29 #endif /*TRICHANNEL_MULTIPLEX_HPP_*/ Listing A.19: The include/fictibot_multiplex/trichannel_multiplex.hpp file. A.3. Fictibot Multiplexer Package 277 1#include <cstdlib> 2#include "fictibot_multiplex/trichannel_multiplex.hpp" 3 4#define LOW_PRIORITY -1 5#define NORMAL_PRIORITY 0 6#define HIGH_PRIORITY 1 7 8TriChannelMultiplexer::TriChannelMultiplexer(ros::NodeHandle& n, double hz) 9: channel_(LOW_PRIORITY) 10 , priority_cycles_(10) 11 , inactivity_counter_(0) { 12 uint32_t queue_size = (uint32_t) hz * 2 + 1; 13 command_publisher_ = n.advertise<std_msgs::Float64>("controller_cmd", queue_size); 14 stop_publisher_ = n.advertise<std_msgs::Empty>("stop_cmd", queue_size); 15 state_publisher_ = n.advertise<std_msgs::Int8>("state", queue_size); 16 high_cmd_subscriber_ = n.subscribe("high_priority_cmd", queue_size, 17 &TriChannelMultiplexer::high_cmd_callback, this); 18 high_stop_subscriber_ = n.subscribe("high_priority_stop", queue_size, 19 &TriChannelMultiplexer::high_stop_callback, this); 20 normal_cmd_subscriber_ = n.subscribe("normal_priority_cmd", queue_size, 21 &TriChannelMultiplexer::normal_cmd_callback, this); 22 normal_stop_subscriber_ = n.subscribe("normal_priority_stop", queue_size, 23 &TriChannelMultiplexer::normal_stop_callback, this); 24 low_cmd_subscriber_ = n.subscribe("low_priority_cmd", queue_size, 25 &TriChannelMultiplexer::low_cmd_callback, this); 26 low_stop_subscriber_ = n.subscribe("low_priority_stop", queue_size, 27 &TriChannelMultiplexer::low_stop_callback, this); 28 std_msgs::Int8 state_msg; 29 state_msg.data = (int8_t) LOW_PRIORITY; 30 state_publisher_.publish(state_msg); 31 } 32 33 void TriChannelMultiplexer::spin() { 34 inactivity_counter_--; 35 if (inactivity_counter_ < 0) { 36 channel_ = LOW_PRIORITY; 37 inactivity_counter_ = priority_cycles_; 38 std_msgs::Int8 state_msg; 39 state_msg.data = (int8_t) LOW_PRIORITY; 40 state_publisher_.publish(state_msg); 41 } 42 ros::spinOnce(); 43 } Listing A.20: The src/trichannel_multiplex.cpp file (part 1 of 3). 284 121 $ref:"#/definitions/ros_type" 122 queue_size: 123 type: integer 124 minimum: 0 125 latched: 126 type: boolean 127 traceability: 128 $ref:"#/definitions/source_location" 129 conditions: 130 $ref:"#/definitions/control_flow_graph" 131 required: 132 - name 133 -type 134 - queue_size 135 - traceability 136 subscribe: 137 type: object 138 properties: 139 name: 140 $ref:"#/definitions/ros_name" 141 type: 142 $ref:"#/definitions/ros_type" 143 queue_size: 144 type: integer 145 minimum: 0 146 traceability: 147 $ref:"#/definitions/source_location" 148 conditions: 149 $ref:"#/definitions/control_flow_graph" 150 required: 151 - name 152 -type 153 - queue_size 154 - traceability 155 advertise_service: 156 type: object 157 properties: 158 name: 159 $ref:"#/definitions/ros_name" 160 type: 161 $ref:"#/definitions/ros_type" 162 traceability: 163 $ref:"#/definitions/source_location" 164 conditions: 165 $ref:"#/definitions/control_flow_graph" 166 required: 167 - name [Document text truncated for crawler view.]