Publications

The methodologies for agile software development are fundamentally based on the collaboration with software users during the entire development process, the simplicity to adapt the product to changes in requirements, and on the incremental product delivery. Based on the Agile Manifesto, they have been accepted and are successfully used in projects where the detailed requirements are unknown at first and are identified during the development process from the interactions with the users and the feedback thus obtained. In this paper, we propose an evaluation framework for the methodologies for agile software development. This framework is applied in detail to two of them - Scrum and eXtreme Programming (XP). The definition of this quantitative framework is innovative, especially because it allows the evaluation of how the agile methodologies satisfy the basic principles defined by the Agile Manifesto, thus it can be used when deciding which methodology to adopt in a particular project. 

Las metodologías de desarrollo ágil se basan fundamentalmente en la colaboración con los usuarios de software durante todo el proceso de desarrollo, la facilidad para adaptar el producto a cambios en requerimientos y en la entrega incremental del producto. Basadas en el Manifiesto Ágil, han sido aceptadas y son utilizadas con éxito en proyectos donde los requerimientos detallados son inicialmente desconocidos y se van construyendo durante el proceso de desarrollo a partir de interacciones con los usuarios y de la retroalimentación obtenida a partir de las mismas. En este trabajo se propone un framework de evaluación para las metodologías ágiles de desarrollo, y se aplica a dos de ellas – Scrum y eXtreme Programming (XP). La definición de este framework cuantitavio es novedosa, especialmente porque permite evaluar en cuánto las metodologías ágiles satisfacen los principios básicos definidos por el Manifiesto Ágil. Su utilización es recomendada al momento de decidir una metodología a adoptar.

We present a model for collaborative problem solving in Virtual Communities of Practice. The model applies a repository, comprising resources, properties and statements, to underpin the process of problem-solving. The process allows for formulating, exploring, matching and gradually refining abstract problem descriptions (one kind of resource) into the corresponding concrete solutions (another kind of resource), expanding the underlying repository with new resources, properties and statements in the process. The model is defined formally, its usefulness is argued with a simple case study and a possible implementation is described using Semantic Web.

 The paper presents a formal model for a knowledge repository shared by members of a Virtual Community of Practice (VCPs), describes how the repository can be used to underpin collaborative problem solving, and how to build computer support for such processes. The repository comprises the resources used and developed by VCPs particularly through problem solving. As a case study, the paper illustrates how the problem solving process and the underlying repository can be applied in disaster prevention and handling. The repository and the process are formally described using the RAISE Specification Language

 We present a model for collaborative problem solving in Virtual Communities of Practice. The model applies a repository, comprising resources, properties and statements, to underpin the process of problem-solving. The process allows for formulating, exploring, matching and gradually refining abstract problem descriptions (one kind of resource) into the corresponding concrete solutions (another kind of resource), expanding the underlying repository with new resources, properties and statements in the process. The model is defined formally, its usefulness is argued with a simple case study and a possible implementation is described using Semantic Web.

 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.

 Free/Libre Open Source Software (FLOSS) projects can be considered as learning environments in which heterogeneous communities get together to exchange knowledge through discussion and put it into practice through actual contributions to software development, revision and testing. This has encouraged tertiary educators to attempt the inclusion of participation in FLOSS projects as part of the requirements of Software Engineering courses, and pilot studies have been conducted to test the effectiveness of such an attempt. This paper discusses two pilot studies with reference to several studies concerning the role of learning in FLOSS projects and shows how using FLOSS projects as E-learning tools has a potential to increase the quality of the software product.

 This paper presents a formalization in the duration calculus (DC) of scheduling policies for tasks with shared resources. Two frameworks are presented for specifying classes of schedulers. With these specifications, some properties of these schedulers were proved using the formal deduction of DC. This paper aims to encourage other researchers to formally treat real-time aspects of operating systems which in the past were conventionally a piece of ad hoc territory in computer science.

The recent intense two-week meeting on trade in endangered species has been described as a failure in many newspapers and blogs, principally because member countries could not reach an agreement on new trade measures to protect certain marine species.

The fifteenth Conference of the Parties (COP15) to the Convention on International Trade in Endangered Species of Wild Fauna and Flora ( CITES) held in Doha, Qatar, included an unprecedented number of proposals regarding commercially exploited aquatic species... 

 Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) which is a subclass of WDC formulas and give an algorithm to check real-time automata for LOI using integer programming. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop techniques to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.

 In this report, we introduce a Probabilistic Duration Calculus (PDC) as a probabilistic extension of Duration Calculus to express dependability requirements for real-time systems, and develop a technique to check a Durational Probabilistic System for a Probabilistic Linear Duration Invariant of PDC.

 Distributed only with authors / publishers permission

 This paper introduces infinite intervals into the Duration Calculus. The extended calculus defines a state duration over an infinite interval by a property which specifies the limit of the state duration over finite intervals, and excludes the description operator. Thus the calculus can be established without involvement of unpleasant calculation of infinity. With limits of state durations, one can treat conventional liveness and fairness, and can also measure out liveness and fairness by properties of limits. Including both finite and infinite intervals, the calculus can, in a simple manner, distinguish between terminate behaviour and nonterminate behaviour, and therefore directly specify and reason about sequentiality.

 The Duration Calculi are calculi for designing real-time software embedded systems. The Calculi overviewed in the paper include the Duration Calculus, the Extended Duration Calculus, the Mean Value Calculus and the Probabilistic Duration Calculus. They are extensions of an Interval Temporal Logic, and can accommodate some concepts of mathematical analysis such as integrals, mean values, piecewise continuity and differentiability of functions over continuous time. The Calculi can be used to capture and refine real-time requirements for hybrid systems, to define real-time behaviour/semantics of computing systems, and to calculate system dependability in terms of requirement satisfaction probability.

 A mean value calculus is presented. It is an extension of the Duration Calculus. The calculus reasons about mean values of durations of Boolean functions instead of integrals. With mean values, we can define integrals and specify point values of functions, and therefore instant actions, including state transitions and events. A state transition of a system determines the system states in a neighbourhood of the transition, and is called a state germ using terminology from topology. State transitions of an automaton are caused by events. Thus the behaviour of an automaton can be formulated by predicates of events and state germs. As an application of the calculus, state germs and their inference rules are introduced and are used to specify and reason about combinational circuits and automata. {\bf Keywords:}Duration Calculus, Mean Value Calculus, State Germs,Combinational Circuit, Automata,Real-Time System.

 This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of {\em linear programming problems}. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.

 Inspired by [He94], a language to describe hybrid systems, i.e. networks of communicating discrete and continuous processes, is proposed. A semantics of the language is given in Extended Duration Calculus [ZRH93], a real-time interval logic with a proof system that allows reasoning in mathematical analysis about continuous processes to be embedded into the logic. The semantics thus provides a secure link to hybrid system models based on a general theory of dynamical systems.