Publications

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.

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.

 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.

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

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.

 Based on an Air Traffic example we illustrate issues of Domain Analysis (of: air space, time tables, and traffic), and of Requirements Capture (of: scheduling systems, and of air traffic control). We relate also to the issue of Software Architecture% (Keynote address: APSEC'95: Asia Pacific Software Engineering Conference, 6--9 December 1995, Brisbane, Australia).

 This is a compendium of 4 papers:

• [(a)] Dines Bjørner. Trustworthy Computing Systems: The ProCoS Experience, February, 1992. Published in: 14th International Conf. on Software Engineering, Melbourne, Australia, May 11-15, 1992, pp. 15-34.
• [(b)] Dines Bjørner and Jørgen Fischer Nilsson. Algorithmic & Knowledge Based Methods -- Do they "Unify"? Published in: International Conf. on Fifth Generation Computer Systems: FGCS'92, Tokyo, June 1-5, 1992 (separate folder, pp. 191-198).
• [(c)] Dines Bjørner. From Research to Practice: Self-reliance of the Developing World through Software Technology -- Usage, Education & Training. Published in: IFIP Transaction, IFIP World Congress '92, Madrid, September 7-11, 1992, pp. 65-71.
• [(d)] Dines Bjørner. A Rôle for UNU-IIST: Developing Countries' Access to New Information Technologies. Presented at: Access to Science and Technology, The Rôle of Information Technology, Kyoto University and UNU Symp., Kyoto, May 12-14, 1992; Expected publ. by UNU Press.

Distributed only with publishers permission

 Before an architecture for a software system (or package) --- that is: a definition of concepts and facilities of the software system (resp.\ package) to be developed --- can be given, one first establishes proper requirements expected of that software, that is: we base software development on requirements specifications. These requirements are captured from understanding first the domain in which the software is to serve and then from understanding the expectations of the new software as an operational part of the thus extended domain. Thus understanding the domain seems to be a very first order of `business'! In this paper we present an example of the collection of (informal) procedures and (formal) techniques that are being applied in understanding the Railway System domain --- as part of a large scale technology transfer project joint with various software development and computer centers of the Chinese Railways in researching and developing proper software eventually for all aspects of railway operation in China.

 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).

 We describe work done at \unuiist\ involving staff from the Chinese railways. The immediate aim is to develop software that can improve the efficiency of the Chinese railway system, particularly in the scheduling of trains. In the longer term we hope to develop the capacity of the Chinese railways to produce and even market their own software. The part of the project described here includes the development of formal models of some basic components of railways (networks of stations and lines and timetables) and the activities needed to schedule and reschedule trains using a \emph{running map}. This part finished with the delivery of a prototype running map tool, and some conclusions are drawn about the formal development of this tool.

Presents the co-ordinates along, and principles according to which UNU-IIST will select and pursue its Programmatic Activities the next couple of years

 Based on an abstract notion of resources, their macro allocation and macro scheduling, we give models of strategic, tactical and operational planning as well as of the actual overall operations of a typical transportation or manufacturing enterprise. We comment on macro- vs. micro allocation and scheduling. The former binds resources to locations and time intervals, the latter binds tasks to (already location allo- cated and interval scheduled) resources. The abstract and the instantiated models are claimed to represent views of classes of application domains and to constitute essential elements of an analysis of such a domain.

 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.