Publications

This paper proposes and investigates an approach to deduction in probabilistic logic, using as its medium a language that generalizes the propositional version of Nilsson's probabilistic logic by incorporating conditional probabilities. Unlike many other approaches to deduction in probabilistic logic, this approach is based on inference rules and therefore can produce proofs to explain how conclusions are drawn. We show how these rules can be incorporated into an anytime deduction procedure that proceeds by computing increasingly narrow probability intervals that contain the tightest entailed probability interval. Since the procedure can be stopped at any time to yield partial information concerning the probability range of any entailed sentence, one can make a tradeoff between precision and computation time. The deduction method presented here contrasts with other methods whose ability to perform logical reasoning is either limited or requires finding all truth assignments consistent with the given sentences.

Artificial agents (AAs), particularly but not only those in Cyberspace, extend the class of entities that can be involved in moral situations. For they can be conceived of as moral patients (as entities that can be acted upon for good or evil) and also as moral agents (as entities that can perform actions, again for good or evil). In this paper, we clarify the concept of agent and go on to separate the concerns of morality and responsibility of agents (most interestingly for us, of AAs). We conclude that there is substantial and important scope, particularly in Computer Ethics, for the concept of moral agent not necessarily exhibiting free will, mental states or responsibility. This complements the more traditional approach, common at least since Montaigne and Descartes, which considers whether or not (artificial) agents have mental states, feelings, emotions and so on. By focussing directly on ‘mind-less morality’ we are able to avoid that question and also many of the concerns of Artificial Intelligence. A vital component in our approach is the ‘Method of Abstraction’ for analysing the level of abstraction (LoA) at which an agent is considered to act. The LoA is determined by the way in which one chooses to describe, analyse and discuss a system and its context. The ‘Method of Abstraction’ is explained in terms of an ‘interface’ or set of features or observables at a given ‘LoA’. Agenthood, and in particular moral agenthood, depends on a LoA. Our guidelines for agenthood are: interactivity (response to stimulus by change of state), autonomy (ability to change state without stimulus) and adaptability (ability to change the ‘transition rules’ by which state is changed) at a given LoA. Morality may be thought of as a ‘threshold’ defined on the observables in the interface determining the LoA under consideration. An agent is morally good if its actions all respect that threshold; and it is morally evil if some action violates it. That view is particularly informative when the agent constitutes a software or digital system, and the observables are numerical. Finally we review the consequences for Computer Ethics of our approach. In conclusion, this approach facilitates the discussion of the morality of agents not only in Cyberspace but also in the biosphere, where animals can be considered moral agents without their having to display free will, emotions or mental states, and in social contexts, where systems like organizations can play the role of moral agents. The primary ‘cost’ of this facility is the extension of the class of agents and moral agents to embrace AAs.

This paper discusses FLOSS communities as a prime example of learning networks, i.e. informal, interconnected sets of individuals mutually supporting shared knowledge acquisition and committed to self-defined goals. In particular, it addresses how the incorporation of a web-based, certification platform for Free / Libre Open Source Software in community culture and practice may increase the community impact both as learning network and open, high-quality software producer.

 It can be argued that participating in free/libre open source software (FLOSS) projects can have a positive effect in the contributor's learning process. The need to interact with other contributors, to read other people's code, write documentation, or use different tools, can motivate and implicitly foster learning. In order to  validate this statement we  design  an appropriate questionnaire asking FLOSS contributors  about their experience in FLOSS projects. In this  paper, we illustrate how this questionnaire was  designed and what we expect to learn from the answers. We conclude the  paper with a preview of the results from three cases studies.

Free and open source software projects are often perceived to be of high quality. To a great extent the success of open source software seems to be due to an implicit but effective connection between communication and contribution in its development process. In this paper, we present a snapshot of the state the art on quality and success of Open Source Software (OSS) based on a review of the literature. For each of these concepts, we describe various measures considered in the literature and a number of methods by which they are obtained. Contributions to an Open Source Software (OSS) project are made through communication among developers and users. We elaborate on the concrete notions of communication and contribution in Open Source Software (OSS) and their links.

Modern societies face high demands for skilled professionals, able to successfully design, deploy and utilize complex Information Technology (IT) –enabled socio-technical systems at everincreasing levels of reliability and security. Contrary to traditional education practices, the high-level training required to fulfill this demand should rely on the principle that the learners are themselves responsible for their learning process, that they have control over this process, and that the process aims at developing cross-disciplinary and problem-driven competences, not only at acquiring content knowledge. However, such training requires the presence of a highly interactive, problem-oriented environment for technology-supported learning (or e-learning). This poster presents a doctoral research project, which aims at designing, validating and monitoring a collaborative e-learning environment based on the principles of Free/Libre Open Source Software (FLOSS). In order to validate its outcomes, the project will rely on two real-life professional training programs: in Software Engineering for software managers and in e-Government for public managers. The poster presents the objectives, research methodology and expected results from this project.

This paper presents a comparative analysis of Free/Libre Open Source Software (FLOSS) Learning Management System (LMS). Following a selection process we analyze the functionalities and characteristics of 8 tools commonly used in formal and informal education. More specifically we focus on the availability of different tools concerning communication and assistance, such as, forum, email, calendar, portfolios, etc. Our analysis showed that despite their similarities, the appropriateness of different FLOSS LMSs can be greatly affected by the specific needs of students, instructors and institutions.

In order to precisely analyze healthcare workflows, we examine how healthcare workflows can be modeled and verified with an elementary and concise timed CSP extension. To avoid considering healthcare workflows in isolation, we investigate the usage of our CSP dialect for formally modeling workflows alongside the instruction model of the openEHR specification set, which is a general, maintainable, and interoperable approach to electronic health records. Hence, we present a CSP model for openEHR instructions, which allows timed reasoning, and also integrates a basic notion of data and undefinedness. We show that this CSP dialect is suited to verify important properties of healthcare workflows, like workflow consistency, checking against timed specifications, and resource scheduling.

The behavior of embedded hardware and software systems is determined by at least three dimensions: control flow, data aspects, and real-time requirements. To specify the different dimensions of a system with the best-suited techniques, the formal language CSP-OZ-DC integrates Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC) into a declarative formalism equipped with a unified and compositional semantics. In this paper, we provide evidence that CSP-OZ-DC is a convenient language for modeling systems of industrial relevance. To this end, we examine the emergency message handling in the European Train Control System (ETCS) as a case study with uninterpreted constants and infinite data domains. We automatically verify that our model ensures real-time safety properties, which crucially depend on the system?s data handling.

We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification.

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.

We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect.

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

In the design process of real-time systems, formal verification establishes global properties of high-level specifications while real-time scheduling analysis ensures that concrete realisations meet essential timing properties with respect to a given target platform. But a formal link between these phases is missing. It is unclear (1) whether timing assumptions that are required to verify properties of high-level specifications can actually be realised on a target platform and (2) whether verified properties remain valid for a schedulable task network. Our approach bridges this gap by guaranteeing that properties verified on specification level are preserved on the implementation level, and vice versa, schedulability results can be propagated back to the specification. To this end, we provide a property-preserving translation from a subclass of the high-level real-time language CSP-OZ-DC into Cyclic Timed Automata, a Timed Automata based task network formalism. We apply our method to a case study from the European Train Control System standard.