Dines Bjørner's University of Tokyo Page
8. Nov. - 8. Dec.: Prof. Tetsuo Tamai Laboratory
While at Tokyo University Dines Bjørner offers to give a two day mini-course .
It is scheduled so that participants may commute both days from locations within the larger Tokyo Area.
While at Tokyo Dines Bjørner offers to give a number (3-4) of seminars and colloquia -- listed below -- at Todai or at other places in Tokyo.
By a seminar we understand the presentation of potentially publishable or published work. By a colloquium we understand the presentation of work in progress, that is, work that still has to find a more "polished" potentially publishable from.
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.
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.
A casual, guided tour through Report Notes.
Abstract: Based on an incomplete report I will discuss issues of modelling a gas or oil pipeline system.
As of November 11, 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.).
A casual, guided tour through Report Notes.
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.
|Todai:MiniC 1/2;Day||Todai:MiniC 2/2;Day|
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 todai
The translation was initiated by Dines Bjorner on 2009-11-11Dines Bjorner 2009-11-11