Search

Modern software relies on libraries and uses them via application programming interfaces (APIs). Correct API usage as well as many software engineering tasks are enabled when APIs have formal specifications. In this work, we analyze the implementation of each method in an API to infer a formal postcondition. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. Our key idea is an algorithm that converts such exponentially large specifications into a form that is more concise and thus more usable. This is done by leveraging the structure of the specifications that result from the use of SP. We applied our technique to infer postconditions for over 2,300 methods in seven popular Java libraries. Our technique was able to infer specifications for 75.7% of these methods, each of which was verified using an Extended Static Checker. We also found that 84.6% of resulting specifications were less than 1/4 page (20 lines) in length. Our technique was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.

Design by Contract (DbC) is a technique for developing and improving functional software correctness through defi- nition of “contracts‿ between client classes and their suppliers. Such contracts are enforced during runtime and if any of them is violated a runtime error should occur. Runtime assertions checkers (RACs) are a well-known technique that enforces such contracts. Although they are largely used to implement the DbC technique in contemporary languages, like Java, studies have shown that characteristics of contem- porary exception handling mechanisms can discard contract violations detected by RACs. As a result, a contract violation may not be reflected in a runtime error, breaking the supporting hypothesis of DbC. This paper presents an error recovery technique for RACs that tackles such limitations. This technique relies on aspect-oriented programming in order to extend the functionalities of existing RACs stop- ping contract violations from being discarded. We applied the recovery technique on top of five Java-based contemporary RACs (i.e., JML/jml, JML/ajml, JContractor, CEAP, and Jose). Preliminary results have shown that the pro- posed technique could actually prevent the contract violations from being discarded regardless of the characteristics of the exception handling code of the target application.

This volume contains the proceedings of the Eight Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2009), affiliated with the 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE). SAVCBS 2009 took place in Amsterdam, Netherlands on August 25, 2009. SAVCBS is focused on using formal (i.e., mathematical) techniques to establish a foundation for the specification and verification of component-based systems. Specification techniques are urgently needed to support effective reasoning about systems composed from components. Component-based approaches also underscore the need for scaling advanced verification techniques such as extended static analysis and model checking to the size of real systems. The workshop considers formalization of both functional and non-functional behavior (such as performance or reliability). SAVCBS aims to bring together researchers and practitioners in the areas of component-based software and formal methods to address the open problems in modular specification and verification of systems composed from components. The workshop seeks to bridge the gap between principles and practice on this research area. The intent of bringing participants together at the workshop is to help form a community-oriented understanding of the relevant research problems and to help steer formal methods research in a direction that will address the problems of component-based systems. The goals of the workshop are to produce: 1. Contacts and discussion among researchers and practitioners, and 2. A web site that will be maintained after the workshop to act as a central clearinghouse for research in this area. We enthusiastically thank the authors of submitted papers; their quality contributions and participation are what make a workshop like SAVCBS successful. We thank the program committee for their careful reading and reviewing of the submissions. Our PC members have expertise in a wide variety of subdisciplines related to specification and verification of component-based systems; they include established research leaders and promising recent Ph.D.s; they come from academia and esteemed research institutes, and hail from all over the world. We received 5 research paper submissions. All papers were reviewed by 3 PC members. After PC discussions, 4 papers were accepted. This year's program also includes solutions to a specification and verification challenge problem for Database libraries. The specification challenge was to specify a core subset of a library as JDBC (java.sql) library (in Java) or ODBC (System.Data and/or System.Data.SqlClient) (in Microsoft ADO.NET), and in particular to address either coordination among related objects, the use of complex, multi-dimensional, multi-modal interfaces, or asynchrony. The verification challenge was to verify an adapter from Apache Beehive that implements an Iterator interface in terms of the JDBC ResultSet. Solutions to the challenge problem are available online via http://www.eecs.ucf.edu/SAVCBS/2009. This year, we are pleased to have a keynote talk by Mariëlle Stoelinga, University of Twente, Netherlands, and an invited talk by Natasha Sharygina, University of Lugano, Switzerland.

Item does not contain fulltext

When dealing with the complex task of extracting meaningful information from multiple continuous sensor streams, declarative rules can be employed to benefit from software engineering principles such as modularization and composition. We propose PARTE, a parallel scalable event processing engine proving predictable response times for a high-quality user experience.