The Webpage of the 3rd International Conference on Runtime Verification is online.

 

RV’2012, September 25 – 28, will be located in the beautiful Istanbul, Turkey.

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness and reliability; they are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for verification and debugging purposes, and after deployment for ensuring reliability, safety and security, and for providing fault containment and recovery.

The deadline to submit to The Third International Workshop on Security Testing, SECTEST’12, is approaching (30 January).

Here is a reminder about SECTEST’s background and objectives:

To improve software security, several techniques, including vulnerability modelling and security testing, have been developed but the problem remains unsolved. On one hand, the workshop tries to answer how vulnerability modelling can help users understand the occurrence of vulnerabilities so to avoid them, and what the advantages and drawbacks of the existing models are to represent vulnerabilities. At the same time, the workshop tries to understand how to solve the challenging security testing problem given that testing the mere functionality of a system alone is already a fundamentally critical task, how security testing is different from and related to classical functional testing, and how to assess the quality of security testing. The objective of this workshop is to share ideas, methods, techniques, and tools about vulnerability modelling and security testing to improve the state of the art.

Link to the homepage of SECTEST’12.

An upcoming exciting event. The Workshop HOWARD-60 dedicated to the anniversary of a good friend: Howard Barringer. This is a very exciting event and a tremendous honor to be an invited speaker.

HOWARD-60 is bringing scientists from both academia and industry together to debate on how to monitor, analyse and guide the execution of programs to ensure their correctness. The ultimate longer term goal is to investigate the use of lightweight formal methods applied during the execution of programs from the following two points of view. On the one hand, whether runtime application of formal methods is a viable complement to the traditional methods proving programs correct before their execution, such as model checking and theorem proving. On the other hand, whether formality improves traditional ad-hoc monitoring techniques used in performance monitoring, distributed debugging, etc. Dynamic program monitoring and analysis can occur during testing or during operation.

The workshop is Festschrift celebrating Howard Barringer’s 60th Birthday and hosted by CICADA and CS, the University of Manchester.

The journal paper More Testable Properties has been recently accepted for publication in the journal Software Tools for Technology Transfer.

This paper is joint work with my friends and colleagues from Verimag (Jean-Claude Fernandez and Laurent Mounier) and from Inria Rennes – Bretagne Atlantique (Thierry Jéron and Hervé Marchand).

The paper shall appear in STTT shortly. One can download a preprint of the paper meanwhile.

Below is an abstract of the paper:

In this article, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties w.r.t. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate a fine-grain characterization of testable properties: for each Safety-Progress class, we identify the subset of testable properties and their corresponding test oracle. Furthermore, we address automatic test generation for the proposed framework by providing a general synthesis technique that allows to obtain canonical testers for the testable properties in the Safety-Progress classification. Moreover, we show how the usual notion of quiescence can be taken into account in our general framework, and, how quiescence improves the testability results. Then, we list some existing testing approaches that could benefit from this work by addressing a wider set of properties. Finally, we propose Java-PT, a prototype Java toolbox that implements the results introduced in this article.

Several research internships are available at LIG laboratory within the VASCO team.

Topics of the internship include (but are not limited to):

  • runtime verification and program monitoring
  • testing
  • Mobile applications (especially Android)
  • web and e-commerce services
  • home-automation

Contact me for more details.

Sep 072011

After almost two great years as a postdoc fellow at INRIA (now Inria) Rennes – Bretagne Atlantique (located in the beautiful French Britanny) within the VerTeCs team, I have moved back to Grenoble.

I get an associate professor position at Grenoble University (University Joseph Fourier) and I am doing my research at LIG – Laboratoire d’Informatique de Grenoble (Computer Science Lab of Grenoble). I am associated to the VASCO team whose speciliaties include software validation (and more particularly testing).

More stuff is forthcoming.

© 2011 Y. Falcone Suffusion theme by Sayontan Sinha