Publications

This volume includes abstracts of the two invited contributions and full papers of the eleven peer-reviewed contributions presented at OpenCert 2010.

 This compendium consists of the papers presented at the FACS'05 workshop. This compendium is the preliminary proceedings for the workshop for the convenience of the workshop participants; the official proceedings will be published after the workshop in the Electronic Notes on Theoretical Computer Science.

 In 1996, Zhou Chaochen and Michael Hansen proposed a first order interval logic called Neighbourhood Logic (NL) which can specify liveness and fairness of computing systems and also define notions of real analysis in terms of expanding modalities introduced therein. Here, we first show that NL forms a sound and complete system. Next, we extend NL by introducing two more expanding modalities in the upward and downward directions and propose a Two Dimensional Neighbourhood Logic (NL$^2$), which can be used to specify super-dense computation. Finally, we also prove completeness of this new NL$^2$ .

Digital libraries (DL) are starting to play a central role in traditional libraries as well as becoming an important tool for publishers to present and sell their products. A lot of research has been carried out to study the usability and data representation in DL and has led to the development of a variety of software packages, both commercial and open source. However, very little research has focused on formal aspects of DL. This paper describes our attempt to formally specify DL using the RAISE Specification Language (RSL). The specification methodology, inspired by the 5S Framework defined by Gonccalves et al. [7], is kept at a fairly abstract level and aims to provide a basic model of the key DL issues (digital objects, collections, users and communities) as well as their relations within the DL framework and the implication of such relations in terms of security and human-computer interactions.

 We present a methodology for modelling population dynamics with formal means of computer science. This allows unambiguous description of systems and application of analysis tools such as simulators and model checkers. In particular, the dynamics of a population of Aedes albopictus (a species of mosquito) and its modelling with the Stochastic Calculus of Looping Sequences (Stochastic CLS) are considered. The use of Stochastic CLS to model population dynamics requires an extension which allows environmental events (such as changes in the temperature and rainfalls) to be taken into account. A simulator for the constructed model is developed via translation into the specification language Maude, and used to compare the dynamics obtained from the model with real data.

 This report is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the concrete and abstract semantics of timed automata (based on transition rules, regions and zones), decision problems, and algorithms for verification. A detailed description on DBM (Difference Bound Matrices) is included, which is the central data structure behind several verification tools for timed systems. As an example, we give a brief introduction to the tool UPPAAL.

 A new semantics of an interesting subset of the specification language SDL is given by a translation to a discrete-time extension of process algebra in the form of ACP with data added as in $\mu$CRL. The strength of the chosen subset, called $\varphi$SDL, is its close connection with full SDL, despite its dramatically reduced size. Thus, we are able to concentrate on solving the basic semantic issues without being in danger of having to turn the results inside out in order to deal with full SDL. Novel to the presented semantics is that it relates the time used with timer setting to the time involved in waiting for signals and delay of signals.

 We present an extension of discrete relative time process algebra where recursion, propositional signals, a counting process creation operator and the state operator are combined. A semantics of $\varphi\!\!^-$SDL, a small subset of SDL that is closely connected with full SDL, is proposed which describes the meaning of $\varphi\!\!^-$SDL constructs using this extension. This semantics allows for the generation of finitely branching transition systems for $\varphi\!\!^-$SDL specifications.

 A process algebra semantics of $\varphi$SDL was given in a previous paper. All behavioural aspects of SDL are covered by $\varphi$SDL, including the time related ones. Here process creation and delaying channels are left out from $\varphi$SDL to concentrate on the process algebraic underpinning of SDL's most distinctive features, viz.\ its communication and timing mechanisms.

 A piece of code in a computer program is infeasible if it cannot be part of any normally-terminating execution of the program. We develop an algorithm for the automatic detection of all infeasible code in a program. We first translate the task of determining all infeasible code into the problem of finding all statements that can be covered by a feasible path. We prove that in order to identify all coverable statements, it is sufficient to find all coverable statements within a certain minimal subset. For this, our algorithm repeatedly queries an oracle, asking for the infeasibility of specific sets of control-flow paths. 

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

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

 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.

 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.

 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.