João Lourenço

Patrícia Monteiro, João Lourenço, António Ravara

--- Portuguese version As falhas de software estão com frequência associadas a acidentes com graves consequências económicas e/ou humanas, pelo que se torna imperioso investir na validação do software, nomeadamente daquele que é crítico. Este artigo endereça a temática da qualidade do software através de uma análise comparativa da usabilidade e eficácia de quatro ferramentas de análise estática de programas em C/C++. Este estudo permitiu compreender o grande potencial e o elevado impacto que as ferramentas de análise estática podem ter na validação e verificação de software. Como resultado complementar, foram identificados novos erros em programas de código aberto e com elevada popularidade, que foram reportados. --- English version Software bugs are frequently associated with accidents with serious economical and/or human consequences, being thus imperative the investment in the validation of software, namely of the critical one. This article addresses the topic of software quality by making a comparative analysis of the usability and efficiency of four static analysis tools for C/C++ programs. This study allow to understand the big potential and high impact that these tools may have in the validation and verification of software. As a complementary result, we identified new errors in very popular open source projects, which have been reported.

Wolfgang Ahrendt, Cyrille Artho, Christian Colombo et al.

This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of the major core aspects involved in Runtime Verification. Runtime Verification is the field of research dedicated to the analysis of system executions. It is often seen as a discipline that studies how a system run satisfies or violates correctness properties. The report exposes a taxonomy of Runtime Verification (RV) presenting the terminology involved with the main concepts of the field. The report also develops the concept of instrumentation, the various ways to instrument systems, and the fundamental role of instrumentation in designing an RV framework. We also discuss how RV interplays with other verification techniques such as model-checking, deductive verification, model learning, testing, and runtime assertion checking. Finally, we propose challenges in monitoring quantitative and statistical data beyond detecting property violation.

Diogo G. Sousa, Ricardo J. Dias, Carla Ferreira et al.

Software developers are expected to protect concurrent accesses to shared regions of memory with some mutual exclusion primitive that ensures atomicity properties to a sequence of program statements. This approach prevents data races but may fail to provide all necessary correctness properties.The composition of correlated atomic operations without further synchronization may cause atomicity violations. Atomic violations may be avoided by grouping the correlated atomic regions in a single larger atomic scope. Concurrent programs are particularly prone to atomicity violations when they use services provided by third party packages or modules, since the programmer may fail to identify which services are correlated. In this paper we propose to use contracts for concurrency, where the developer of a module writes a set of contract terms that specify which methods are correlated and must be executed in the same atomic scope. These contracts are then used to verify the correctness of the main program with respect to the usage of the module(s). If a contract is well defined and complete, and the main program respects it, then the program is safe from atomicity violations with respect to that module. We also propose a static analysis based methodology to verify contracts for concurrency that we applied to some real-world software packages. The bug we found in Tomcat 6.0 was immediately acknowledged and corrected by its development team.