Publications

This volume includes abstracts of the two invited contributions and full papers of the eleven peer-reviewed contributions presented at OpenCert 2010.

 Over the last decade, the importance of Free/Libre/Open Source Software (FLOSS) has increased dramatically and the size and scope of the OSS conference within which this workshop takes place is testament to that reality. This volume contains the proceedings of the joint workshop: the first International Workshop on Foundations and Techniques bringing together Free/Libre/Open Source Software and Formal Methods (FLOSS-FM 2008) and the second International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2008). All submitted papers have been reviewed by at least 3 Program Committee members. The aim of the workshop has been to bring together researchers from academia and industry, firstly, to study the question of FLOSS certification and, secondly, to explore in the largest possible sense the question of how formal methods can be brought more successfully to bear on the open source phenomenon, and also how FLOSS can be brought more fully into the formal methods community. The organisers would like to take this opportunity to thank the contributors, the programme committee and all the referees for their interest and hard work. We leave to the reader the seeds the participants have sown.

Understanding the behaviour of biological systems requires a complex setting of in vitro and in vivo experiments, which attracts high costs in terms of time and resources. The use of mathematical models allows researchers to perform computerised simulations of biological systems, which are called in silico experiments, to attain important insights and predictions about the system behaviour with a considerably lower cost. Computer visualisation is an important part of this approach, since it provides a realistic representation of the system behaviour. We define a formal methodology to model biological systems using different levels of representation: a purely formal representation, which we call molecular level, models the biochemical dynamics of the system; visualisation-oriented representations, which we call visual levels, provide views of the biological system at a higher level of organisation and are equipped with the necessary spatial information to generate the appropriate visualisation. We choose Spatial CLS, a formal language belonging to the class of Calculi of Looping Sequences, as the formalism for modelling all representation levels. We illustrate our approach using the budding yeast cell cycle as a case study. 

This paper describes preliminary results on the application of statistical model-checking to systems described with Stochastic CLS. Stochastic CLS is a formalism based on term rewriting that allows biomolecular systems to be described by taking into account their structure and by allowing very general events to be modelled. Statistical model-checking is an analysis technique that permits properties of a system to be studied on the results of a number of stochastic simulations. We choose Real-Time Maude as a tool that supports the modelling and analysis of systems with real-time properties. We adapt Gillespie's algorithm for simulating chemical systems into our approach. The resulting method is applied to analyse some simple examples and a model of the lactose operon regulation in E.coli.

 We present a methodology for modelling population dynamics with formal means of computer science. This allows unambiguous description of systems and application of analysis tools such as simulators and model checkers. In particular, the dynamics of a population of Aedes albopictus (a species of mosquito) and its modelling with the Stochastic Calculus of Looping Sequences (Stochastic CLS) are considered. The use of Stochastic CLS to model population dynamics requires an extension which allows environmental events (such as changes in the temperature and rainfalls) to be taken into account. A simulator for the constructed model is developed via translation into the specification language Maude, and used to compare the dynamics obtained from the model with real data.

 This article describes a framework to formally model and analyse human behaviour. This is shown by a simple case study of a chocolate vending machine, which represents many aspects of human behaviour. The case study is modelled and analysed using the Maude rewrite system. This work extends a previous work by Basuki which attempts to model interactions between human and machine and analyse the possibility of errors occurring in the interactions. By redesigning the interface, it can be shown that certain kinds of error can be avoided for some users. This article overcomes the limitation of Basuki’s approach by incorporating many aspects of user behaviour into a single user model, and introduces a more natural approach to model human–computer interaction. 

Digital libraries (DL) are starting to play a central role in traditional libraries as well as becoming an important tool for publishers to present and sell their products. A lot of research has been carried out to study the usability and data representation in DL and has led to the development of a variety of software packages, both commercial and open source. However, very little research has focused on formal aspects of DL. This paper describes our attempt to formally specify DL using the RAISE Specification Language (RSL). The specification methodology, inspired by the 5S Framework defined by Gonccalves et al. [7], is kept at a fairly abstract level and aims to provide a basic model of the key DL issues (digital objects, collections, users and communities) as well as their relations within the DL framework and the implication of such relations in terms of security and human-computer interactions.

 Reducing the likelihood of human error in the use of interactive systems is increasingly important: the use of such systems is becoming widespread in applications that demand high reliability due to safety, security, financial or similar considerations. Consequently, the use of formal methods in verifying the correctness of interactive systems should also include analysis of human behaviour in interacting with the interface. This report includes pre-event versions of all papers accepted for presentation at the 1st International Workshop on Formal Methods for Interactive Systems (FMIS 2006) held on 31 December 2006 in Macau SAR China, as a satellite event of ICFEM 2006. FMIS 2006 is organized by UNU-IIST in collaboration with the Human Error Modeling (HUM) project sponsored by EPSRC on research grants GR/S67494 and GR/S67500. The aim of this workshop is to bring together researchers in computer science and cognitive psychology, from both academia and industry, who are interested in developing formal and semi-formal methodologies and tools for the evaluation and verification of interactive systems. The outcome is to establish a worldwide network of researchers interested in applying formal methods to HCI. The workshop focuses on general design and verification methodologies based on cognitive psychology as well as application areas such as mobile devices, embedded systems, safety-critical systems, high-reliability systems, shared control systems, digital libraries, eGovernment, pervasive systems, augmented reality. All papers submitted to the workshop were reviewed by 3 referees followed by a meta-review process. From the 18 submissions the Program Committee selected 6 papers for long presentation (40 minutes) and 2 papers for short presentation (20 minutes). Revised versions of the 6 papers accepted for long presentations will be published after the workshop by Elsevier B. V. in the Electronic Notes in Theoretical Computer Science Series. The authors of the most relevant papers presented at the workshop will be invited to submit extended versions of their papers to be considered for publication in a special issue of a journal. In addition to contributed papers, the workshop programme also includes a keynote talk by Harold Thimbleby from the University of Wales, Swansea. His presentation is entitled "Building dependable interactive systems" and uses medical devices as a case study to discuss the problems of making interactive systems dependable. It introduces suggestions for improving them, particularly by using formal methods.

Software quality is more than just conformance to a set of requirements and represents many attributes related to each other that make up a piece of software. An important part of this measure depends on the underlying processes and methodologies used in the engineering of software. We present an early exposition towards a quality model for open source software (OSS). We describe some basic notions of quality for OSS and present a basic model, where quality notions consist of various factors that influence such quality. The purpose of this effort is ultimately to develop a quantitative metric for software quality.

The majority of Free and Open Source Software (FOSS) developers are mobile and often use different identities in the projects or communities they participate in. These characteristics not only poses challenges for researchers studying the presence (where) and contributions (how much) of developers across multiple repositories, but may also require special attention when formulating appropriate metrics or indicators for the certification of both the FOSS product and process. In this paper, we present a methodology to study the patterns of contribution of 502 developers in both SVN and mailing lists in 20 GNOME projects. Our findings shows that only a small percentage of developers are contributing to both repositories and this cohort are making more commits than they are posting messages to mailing lists. The implications of these findings for our understanding of the patterns of contribution in FOSS projects and on the quality of the final product are discussed.

 Business Process Execution Language (BPEL), or Web Services BPEL (WS-BPEL), is the standard for specifying workflow process definition using web services. Research on formal modelling and verification of BPEL has largely concentrated on control flow and data flow, while security related properties have received little attention. In this work, we present a formal framework that integrates Role Based Access Control (RBAC) into BPEL and allows us to express authorisation constraints using temporal logic. Using this framework, we show how model-checking can be applied to verify that a given BPEL process satisfies the security constraints.