MSVVEIS 2012 Abstracts

Full Papers
Full Papers
Paper Nr: 1
Title:

Coverage based Test Generation for Duration Systems
Authors:

Maha Naceur, Lotfi Majdoub and Riadh Robbana
Abstract: In this paper, we are interested in generating test cases for duration systems with respect to coverage criteria. Duration systems are an extension of real-time systems for which delays that separate events depend on the accumulated times spent by the computation at some particular locations of the system. We present a test generation method for duration systems by considering coverage criteria. This method uses the approximation approach and extends a model using an over approxima- tion, the approximate model, containing the digitization timed words of all the real computations of the duration system. Then, we propose an algorithm that generates a set of test cases presented with a tree by considering a discrete time and respecting a coverage criterion in order to select test cases.
Download
Paper Nr: 3
Title:

A Compositional Scheme and Framework for Safety Critical Systems Verification
Authors:

Manuel I. Capel and Luis E. Mendoza-Morales
Abstract: Safety--Critical Systems (SCS) must satisfy dependability requirements such as availability, reliability, and real-time constraints, in order to justify the reliance of the critical service they deliver. A verification framework named 'Formal Compositional Verification Approach' (FCVA) is presented here. FCVA establishes a compositional method to verify safety, fairness and deadlock absence of SCS. Software components of a given critical system are model--checked to verify the aforementioned properties. Our objective in this paper is to facilitate the design of an SCS from a collection of verified simpler components, and hence allowing complete complex SCS software verification. An application on a real--life project in the field of mobile phone communication is discussed to demonstrate the applicability of FCVA.
Download
Paper Nr: 4
Title:

Empirical Comparison of Comprehensibility of Requirement Specification Techniques based on Natural Languages and Activity Diagrams
Authors:

Bogumila Hnatkowska and Mateusz Grzegorczyn
Abstract: Understandability belongs to the most important features of good quality software requirement specification (SRS) . There exist plenty notations used for defining SRS, but still natural language (NL) belongs to the most pop-ular. The specification written is NL could suffer from ambiguity, however it can be read by everybody without specific training. To eliminate, even partially, the drawbacks mentioned previously, SRS is written according to well defined guidelines and with the use of templates, e.g. use-case model consisting of a use-case diagram with a set of use-case detailed descriptions. Use-case descriptions are defined in NL or with dynamic diagrams, e.g. activity diagrams. This paper presents a controlled experiment which aimed at comparison of comprehensibility of techniques based on natural language and activity diagrams. The results of the experiment confirmed that formal notation is less ambiguous. Additionally, if a reader is accustomed to it, reading activity diagram not necessarily is time consuming.
Download
Paper Nr: 6
Title:

Testing Temporal Logic on Infinite Java Traces
Authors:

Damián Adalid, Alberto Salmerón, María del Mar Gallardo and Pedro Merino
Abstract: This paper presents an approach for testing reactive and concurrent Java programs which combines model checking and runtime monitoring. We use a model checker for two purposes. On the one hand, it analyzes multiple program executions by generating test input parameters. On the other hand, it checks each program execution against a linear temporal logic (LTL) property. The paper presents two methods to abstract the Java states that allow efficient testing of LTL. One of this methods supports the detection of cycles to test LTL on potentially infinite Java execution traces. Runtime monitoring is used to generate the Java execution traces to be considered as input of the model checker. Our current implementation in the tool TJT uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as a plug-in for Eclipse and it has been successfully applied to complex public Java programs.
Download