Dines Bjørner's Edinburgh Page
Dines Bjørner is a SICSA Distinguished Visitor 21.Sept.-30.Oct.2009.
While at Edinburgh Dines Bjørner offers to give a two day mini-course at Edinburgh.
It is scheduled so that participants may commute both days from locations outside Edinburgh.
While at Edinburgh Dines Bjørner offers to give a number of seminars and colloquia -- listed below -- at Edinburgh and at collaborating SICSA institutions.
First Draft, Incomplete Paper
Abstract: This paper is for the academic who is interested in a philosophy of science and a theory of science. The paper proposes some features of a philosophy of informatics and a theory of the science of informatics. We approach some such features by first outlining, in "lay" terms, concepts of computer and computing science, informatics and of a triptych of domains, requirements and software. Domains are a new concept in informatics. We briefly illustrate that domains can be described both informally, that is, using natural (cum national) language, and formally, in mathematics. Then we discuss a number of concepts common to all domains, their simple entities, functions, events and behaviours. We then go on to examine some derivative concepts of these: discrete and continuous as well as atomic and composite entities and the mereology of composite entities, Finally we discuss (i) the problem of description in the context of Bertrand Russell's `Philosophy of Logical Atomism', (ii) the problem of describing parts and wholes in the context of Stanisaw Leshniewsky's `Mereology' and Individuals', and (iii) a possible set of domain description laws. This is our second attempt at discussing aspects of an emerging philosophy of informatics -- some might call it dabbling into such issues. A first attempt was a paper for the journal of Higher Order and Symbolic Computation, for a fall 2009 issue in honour of the late Peter Landin. The reader should thus bear with us firstly because of our lack of deeper experience in matters of philosophy, secondly because we only treat a few facets and then only hint at them. We shall therefore be grateful for any suggestions from readers, and we are likewise grateful to The University of St Andrews for asking me to compose my thoughts on this issue.
Paper - Slides
Abstract: We introduce the notion of domain descriptions (D) in order to ensure that software (S) is right and is the right software, that is, that it is correct with respect to written requirements (R) and that it meets customer expectations (D). That is, before software can be designed (S) we must make sure we understand the requirements (R), and before we can express the requirements we must make sure that we understand the application domain (D): the area of activity of the users of the required software, before and after installment of such software. We shall outline what we mean by informal, narrative and formal domain descriptions, and how one can systematically -- albeit not (in fact: never) automatically -- go from domain descriptions to requirements prescriptions. As it seems that domain engineering is a relatively new discipline within software engineering we shall mostly focus on domain engineering and discuss its necessity. The talk will show some formulas but they are really not meant to be read, let alone understood. They are merely there to bring home the point: Professional software engineering, like other professional engineering branches rely on and use mathematics. And it is all very simple to learn and practise anyway ! We end this talk with, to some, perhaps, controversial remarks: Requirements engineering, as pursued today, researched, taught and practised, is outdated, is thus fundamentally flawed. We shall justify this claim.
Abstract: In this talk we solve the following problems:
We have yet to prove to what extent the models satisfy the axiom systems for mereologies of, for example, (Casati&Varzi1999) and a calculus of individuals (Bowman&Clarke1981). Mereology is the study, knowledge and practice of part-hood relations: of the relations of part to whole and the relations of part to part within a whole. By parts we shall here understand simple entities -- of the kind illustrated in this talk.
Manifest simple entities of domains are either continuous (fluid, gaseous) or discrete (solid, fixed), and if the latter, then either atomic or composite. It is how the sub-entities of a composite entity are ``put together'' that ``makes up'' a mereology of that composite entity -- at least such as we shall study the mereology concept. In this talk we shall study some ways of modelling the mereology of composite entities. One way of modelling mereologies is using sorts, observer functions and axioms (McCarthy style), another is using CSP.
A Role for Bertrand Russell's Philosophy of Logical
and Stanislaw Leshniewski's Mereology
Abstract: Domain engineers describe universes of discourse such as bookkeeping, the financial service industry, container shipping lines, logistics, oil pipelines, railways, etc. In doing so domain engineers have to decide on such issues as identification of that which is to be described; which of the describable phenomena and concepts are (to be described as) entities, operations, events, and which as behaviours; which entities are (to be described as) continuous which are (...) discrete, which are (...) atomic, which are (...) composite and what are the attributes of either and the mereology of composite entities, i.e., the way in which they are put together from sub-entities. For each of these issues and their composite presentation the domain engineer has to decide on levels of abstraction, what to include and what to exclude.
In doing so the domain engineer thus has to have a firm grasp on the a robust understanding and practice of the very many issues of description: what can be described, identifying what is to be described, how to describe, description principles, description techniques, description tools and laws of description. This talk will outline the issues in the slanted type font.
One issue, `mereology', was studied, in a wider setting, by the Polish philosopher and mathematician Stanisaw Leshniewski, in the 1920s (Lesniewski1,Lesniewski3). We shall relate our work to that of Leshniewski and those of his followers who have suggested axiomatisations of various forms of mereology (LeonardGoodman1940, BowmanLClarke81, Lejewski83, BowmanLClarke85, CasatiVarzi1999).
Similar issues, it appears, were studied, also in a wider setting, by Bertrand Russel in his lectures in 1918 and published in the Monist Journal, vols. XXVIII-XXIX in 1918-1919. In this essay we shall sketch how we see the role of "applied logical atomism" in domain engineering.
Paper - Slides
Abstract: The triptych approach to software engineering proceeds on the basis of carefully monitored and controlled possibly iterated progression through domain engineering and requirements engineering to software design.
In this talk I will outline these three phases, show the many stages of development within each and also indicate the many steps within each stage. We will ever so briefly touch upon informal narration and formal description (prescription and specification) of domains (requirements and software designs), and the verification (theorem proving, model checking and testing) and validation of domain descriptions (requirements prescriptions and their relations to domain descriptions, as well as the software design specifications and their relations to requirements prescriptions). The importance of process management and its relations to software process assessment (SPA) and software process improvement (SPI) will then be underscored. Our measuring ``stick'' is that set up by Watts Humphrey's capability maturity model (CMM). We will suggest and discuss seven assessment and eight improvement categories. In closing we will have some few words to say about software procurement.
Abstract: We analyse the domain of IT systems and `add' to that domain the concept of IT Security Rules (and Regulations). The analysis is done, first informally, then formally. The informal analysis and its presentation follows the `dogmas' set out in Vol.3 of Software Engineering. The formal presentation follows the principles and techniques and uses the tools outlined in Vols.1-2 of the afore-mentioned book.
Research Topic: I wish to (i) study transliteration of ISO IT Security Recommendation texts into FOL predicates, (ii) study that text's implicit assumptions about the context in which these recommendations apply, and (iii) study formal models of such contexts in which the FOL predicates can be interpreted.
Abstract: Classical digital rights license languages, applied to the electronic "downloading", payment and rendering (playing) of artistic works (for example music, literature readings and movies). In this talk we generalise such applications languages and we extend the concept of licensing to also cover work authorisation (work commitment and promises) in health care and in public government. The digital works for these two new application domains are patient medical records, public government documents and bus transport contracts.
Digital rights licensing for artistic works seeks to safeguard against piracy and to ensure proper payments for the rights to render these works. Health care and public government license languages seek to ensure transparent and professional (accurate and timely) health care, respectively `good governance'. Bus transport contract languages seeks to ensure timely and reliable bus services by an evolving set of transport companies.
Proper mathematical definition of licensing languages seeks to ensure smooth and correct computerised management of licenses and contracts.
In this talk we shall motivate and exemplify four license languages, the pragmatics and syntax of four of them as well as the formal semantics of one of them.
Abstract: Based on an incomplete report I will discuss issues of modelling a gas or oil pipeline system.
As of October 2, 2009 this document has the status of ``report on an [advanced engineering] experiment''. By `advanced engineering' we mean that the engineering has a non-trivial element of applied research: at the outset of this `experiment' we do not know ``how it will all turn out''.
Its purpose is to record considerations of how to model the statics and dynamics of an oil (or gas) pipeline system: of integrating a model-oriented formal specification (expressed in RSL) with a property-oriented formal specification (expressed in the Duration Calculus).
It is hoped that one part of the experiment will have at least the following effects: (i) the positive testing of the domain engineering paradigm as expressed in a number of publoshed papers and books; (ii) the addition to the methodology of domain engineering of a number of modelling principles, techniques and tools -- notably that of the Duration Calculus; and (iii) the further exemplification of uses of the Duration Calculus.
Based on preliminary models of the semantics of oil pipeline systems we propose a language of (syntactic) pipeline systems, ascribe a semantics to this language, and, hopefully also some proof rules that will allow us to reason about planned, actual oil pipeline systems.
In preparation for the semantic model of the language of (syntactic) pipeline systems we ``compile'' syntactic versions of the semantic oil pipelin systems into sets of communicationg sequential processes (in RAISE/CSP).
We further aim at ``lifting'' the target domain to that of the more conceptual domain of ``flows in networks'' (FordFulkerson62) (to wit: waterways, freight transport nets, etc.).
Abstract: Based on an incomplete report I will discuss issues of modelling a logistics.
We examine the concept of logistics, exemplify it by some ``use cases'', bring a definition of the term `logistics' from Wikipedia What is Logistics), and then we rigorously and stepwise unravel the constituent concepts of Transport Networks Containers and Freight Items, Transport Companies, Vehicles and Timetables, Handling, Logistics Traffic and Senders and Receivers. Towards the end, Model Extensions, we discuss possible additional phenomena and concepts of logistics. The talk presents a domain model (in the form of a both English narrative and a formal description), that is, it does not present requirements to a computerised logistics system, let alone software for such systems.
We constrain the treatment of logistics to that of shipping companies handling (optimal) freight consignments (cf. waybills and bill of ladings) involving possibly multiple vehicles from possibly multiple transport companies. Thus we do not cover the logistics of, say, container stowage aboard container vessels. In http://www.imm.dtu.dk/~db/container-paper.pdf we cover that aspect.
Abstract: Based on an incomplete (98 page) report I will discuss issues of modelling a a container line industry.
This survey talk is primarily about domain modelling. The following facets of domain modelling will be covered: business processes, intrinsics, support technologies, management and organisation, rules and regulations, scripts, and human behaviour. The survey talk will exemplify excerpts of models of container shipping, financial services, etcetera. We shall relate two (of three) parts of requirements models to domain models: the domain requirements - which are the requirements that can be expressed solely in terms of the terms of the domain models, and the interface requirements - which are those requirements that can only be expressed using terms both of the domain and the machine: the hardware and software being required. For domain requirements we briefly sketch the domain-to-requirements ``algebra'' of projection, instantiation, determination, extension and fitting. For interface requirements we briefly sketch the domain & machine issues of shared entities (bulk data input and refreshments), shared functions, shared events, and shared behaviours.
|Bank||Rod Burstall 2pm||Lilia Georgieva 4pm|
|Holiday||George Hay 3:30pm||Welcome Dinner 6pm||Off to Oban 3:25pm|
|EU[G.03]MiniC 1/2:am||EU[G.03]MiniC 2/2:am|
|EU[G.03]MiniC 1/2:pm||EU[G.03]MiniC 2/2:pm||HW[G44],1,2:15pm||Off to Kilin 4pm|
|HW[G45],4,2:15pm||CPH Flight 4:50pm||NWPT||Edinburgh Flight 8:15-9:15pm|
|GU,1,4:00pm||Off to Inverness 4:33pm|
For further information about Dines Bjørner please click one or more of the below items:
This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)
Copyright © 1993, 1994, 1995, 1996,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -toc_depth 5 edinburgh
The translation was initiated by Dines Bjorner on 2009-10-02Dines Bjorner 2009-10-02