Publications

 We study the concept of Problem Frames first suggested by Michael A. Jackson. For each of a number of Problem Frames we suggest an explanation of that Frame in terms of the set of application Domains, the set of Requirements and the set of Designs that seem to best characterise it. For each we give graphic and formal characterisations. Our presentation also focuses on the Syntax, Semantics and Pragmatics of Problem Frames.

 The aim of this mostly analytical paper is to propose a definition of {\sl what an infrastructure is.\/} This definition will be stated in terms of properties of properties of mathematical models of the domain of the `infrastructure', in terms of properties of requirements put to computing \& communications support, and in terms of characteristics of possible architectures for software that support the `infrastructure'. The paper is presently in draft form, but is circulated in order to solicit comments. Eventually a version of the paper will be presented at the Spring Session of the Mathematics and Informatics Section of {\sf Academia Europaea}, 11--12 April 1996 in Amsterdam, The Netherlands.

 This paper is part speculative, part technical, and mostly discursive! The paper is also comprehensive and should be readable by a large fraction of the software community. The conjectures of the paper are based on more than 30 years of extensive experience in computing and software systems development: in the formal, abstract specification of software system architectures, and in their stepwise implementation. The conjecture of the paper is this: For a software house, a producer of products, to be able, in future, to compete effectively it must possess: (i) deep and broad (large scale) problem domain knowledge represented in the form of `mathematical theories of application domains', (ii) ready access to `software devices and mechanisms', and (iii) otherwise pursue development steadily using a large variety of `design calculi'. The paper will define the single-quoted concepts, and will illustrate large-scale applications.

 We define and motivate the need for research into, advanced development and actual deployment, by public and private sector institutions and enterprises, of an advanced class of uses of geographically widely distributed information technology systems of computers and communications in achieving {\sl software support for infrastructure systems} (This paper represents the \unuiist\ position statement for the {\sf Infotech Malaysia '95} National Conference to be held in Kuala Lumpur (and otherwise video broadcast across Malaysia, 1--3 November 1995)).

 In this paper we review (i) basic functions of gapa with respect to its possible needs for computers and communications (Henceforth we will abbreviate computer and communications by cac.) (notably software); (ii) the basic tasks confronting upper level management of papa institutions when considering cac; (iii) the basic tasks confronting cac facilities management when procuring, monitoring the development of and operating new software technology for gapa; and (iv) the basic tasks confronting {\sf New Development of Software Technology}. In this latter we cover current thoughts on software development process modeling, current methods, principles, techniques, and tools of software development. We need to cover (i--iii) in order to properly understand the setting for and offerings of what is covered in (iv) (Special {\sl Theme\/} paper. {\sf New Software Technology Development} first prepared in September 1995 for an International Symposium: {\sf New IT Applications for Governance and Public Administration}, convened by the UN's Department for Development Support and Management Service: UNDDSMS, Beijing, November 9--14, 1995. This symposium was subsequently moved (tentatively) to June 1996, same venue).

Delta-oriented programming allows software developers to define software product lines as variations of a common code base, where variations are expressed as so-called program deltas. Monitor-oriented programming (MOP) provides a mechanism to execute functionality based on the program's execution history; this is useful, e.g., for the purpose of runtime verification and for enforcing security policies.

 This compendium consists of the papers presented at the FACS'06 workshop.

 The purpose of this paper is to explore the models and forms of reasoning appropriate for analysing the temporal behaviour of circuits. That leads from various Boolean models appropriate for combinational and synchronous circuits, to the event model for asynchronous circuits. Circuit behaviour is captured at each level of abstraction using model-specific operators, whose laws are used to perform algebraic (rather than semantic) reasoning about transient behaviour. The results have a particularly satisfying form: for example the hazards of a conditional are calculated algebraically to be a conditional of hazards. A method is developed for simulating an asynchronous combinational circuit, that starts with an untimed, logic-level, specification, passes to a timed refinement and then moves to a simple timed automaton for simulation in UPPAAL. Each stage in the method is supported by a projection relating the models at the various levels, so that correctness can be confirmed.

Graph transformation techniques, and the Double-Pushout (DPO) approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this report, we provide a theory of graph transformations for service programming with sessions and pipelines. The theory shows how graph transformation can cope with advanced features of service-oriented computing, such as several logical notions of scoping (like sessions and pipelines) together with the interplay between linking and containment. This is illustrated by encoding CaSPiS, a recently proposed process calculus with such sophisticated features. We first exploit a graph algebra and set up a graph model that supports DPO graph transformations. Then, we show how to represent CaSPiS processes as hierarchical graphs in the graph model and their behaviors as transformation rules over these graphs. Finally, we provide the soundness and completeness results of these rules with respect to the reduction semantics of CaSPiS.

Graph transformation techniques, and the Double-Pushout approach in particular, have been particularly successful in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we show how graph transformation can cope with advanced features of service-oriented process calculi, such as several logical notions of scoping (sessions, pipelines), pattern matching together with the interplay between linking and containment. This is illustrated by encoding CaSPiS, a recently proposed process calculus with such sophisticated features. We show how to handle congruence rules and reduction rules using a suitable notion of hierarchical graphs. The main result proves soundness and completeness of the encoding with respect to congruence.

Graph transformation techniques, and the Double-Pushout approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we show how graph transformation can cope with advanced features of service-oriented process calculi, such as several logical notions of scoping (like sessions and pipelines) together with the interplay between linking and containment. This is illustrated by encoding CaSPiS, a recently proposed process calculus with such sophisticated features. We show how to represent the congruence and reduction relations between CaSPiS processes by exploiting concurrent graph transformations over hierarchical graphs.

 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.

 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