Cláudio Belo Lourenço

Spectrum-based fault localization (SFL) and dynamic code coverage (DCC) are two statistics-based fault localization techniques used in software fault diagnosis. Due to their nature (statistical analysis of the coverage information), the best technique of the two depends greatly on the system under test code structure and size. We propose a lightweight, topology-based analysis to quickly estimate the project under test coverage matrix when executed, based on the source code structure. This analysis will choose which fault localization technique to use by creating an hierarchical model of the system. To validate our proposed approach, an empirical evaluation was performed, injecting faults in six real-world software projects. We have demonstrated that using the topology-based analysis to choose the best fault localization technique provides a better execution time performance on average (23%) than using DCC (9%), when comparing to SFL.

Despite the enhancement on software hardness induced by development-time automatic testing and debugging tools, it remains practically impossible to create fault-free applications. The research on self-healing systems emerged to enable applications to cope with unexpected events at run-time in order to maximize their availability, survivability, maintainability, and reliability, while minimizing human intervention. With the increase in software's complexity, in part triggered by the advent of the Internet and Cloud Computing, self-healing properties in applications are becoming a necessity. The main focus of this position paper is on presenting the issues that render unusable or ineffective the usage of the development-time Spectrum-based Fault Localization(SFL) algorithm in run-time environments. We concluded that, despite the issues found, it should be possible to devise an SFL algorithm for run-time environments that can also achieve the good results yielded by SFL at development-time.

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness of the task scheduler component of the FreeRTOS kernel using the verification system HIP/SLEEK. We show how some of HIP/SLEEK features like user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that HIP/SLEEK can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify the scheduler of other operating systems.

Synchronous coordination systems, such as Reo, exchange data via indivisible actions, while distributed systems are typically asynchronous and assume that messages can be delayed or get lost. To combine these seemingly contradictory notions, we introduce the Dreams framework. Coordination patterns in Dreams are described using a synchronous model based on the Reo language, whereas global system behaviour is given by the runtime composition of autonomous actors communicating asynchronously. Dreams also exploits the use of actors in the composition of coordination patterns to allow asynchronous communication whenever possible, increasing the scalability of the implementation.

Since wireless sensor network applications are ever growing in scale and complexity, managers require strong formal guarantees that any changes done to the system can be enacted safely. This paper presents the formalisation and analysis of the semantics of policies, tiny software artefacts used to orchestrate wireless sensor network applications. The semantics of policies is formalised in terms of traces augmented with information concerning the constraints under which traces are executed. These traces are composed according to the network topology and subsequently analysed using them CRL2 model-checking tool. The analysis allows for the detection of semantical inconsistencies that may lead to dangerous or unwanted behaviour of the application based on the policy configuration. An analysis of policies in a real-world system is provided, showing how to verify security and resource usage properties.

With the rapidly increasing over 60 and over 80 age groups in society, greater emphasis will be put on technology to detect emergency situations, such as falls, in order to promote independent living. This paper describes the development and deployment of fall-detection, activity classification and energy expenditure algorithms, deployed in a tele-monitoring system. These algorithms were successfully tested in an end-user trial involving 9 elderly volunteers using the system for 28 days.