In nine lectures we intend to introduce a number of facets of computing science and software engineering. They are: (1) the both property- and model-oriented formalisation of what is described, prescribed or specified; (2) software engineering as properly proceeding from domain descriptions via requirements prescriptions to software specification and implementation; (3) attempts to establish domain theories, in this case for transportation; and (4) - more narrowly - Petri nets, message sequence charts (MSCs) and communicating transaction processes (CTPs).
NARRATION AND FORMALISATION OF STATICS OF RAILWAY NETS
We cover rail nets as consisting of stations and lines, and these as consisting of linear, simple switch, crossover, double slip crossover, and other rail units, and rail units as embodying a concept of connectors.
The formalisation introduces us to property-oriented formal specification in terms of algebraic sorts, observer (and generator) functions, and axioms, as to model-oriented formal specification in terms of sets, Cartesians, lists, maps, types, etc.
ON A SOFTWARE ENGINEERING TRIPTYCH
Before software can be designed its requirements must be understood.
Before requirements can be formulated one must understand the (application) domain.
We outline facets of domain models: intrinsics, business processes, support technologies, management & organisation, rules & regulations, scripts and human behaviour.
NARRATION AND FORMALISATION OF DYNAMICS OF RAILWAY NETS AND TRAIN TRAFFIC
We cover states of rail units, open and closed routes, reachability of station tracks from lines and vice-versa, and net dynamics.
We cover train movement, train traffic and their well-formedness, time tables and relations between train traffic and time tables.
NARRATION AND FORMALISATION OF OTHER RAILWAY SYSTEM ISSUES
Regularly, round-the-clock trains need have their individual cars regularly serviced, not all at the same time, and not all at the same maintenance yard. Hence a train time table must ensure that any train car whose visit to a maintenance yard is up are close to, or in that yard.
We narrate the problem and highlight possible formalisation.
Trains are staffed and staff need travel to and from stations to commence and end their tours of duty. Many constraints govern which staff can go on what trains, where and when.
We narrate the problem and highlight possible formalisation.
A proper passenger statistics show, for suitable round-the-clock time intervals which numbers of passengers wish to travel, or are actually travelling between which small or large centers of population.
A rail-net can be characterised wrt. its optimality in affording implied travels, and a time table can likewise be characterised wrt. its optimality in actually offering such travels.
We narrate the problem and highlight possible formalisation.
Commuter trains oftentimes travel fairly long distances. And usually such commuter trains undergo changes in their composition of passenger cars during their travel. Problems of affording simple coupling and decoupling of cars at stations, depending on the travel direction and whether a station forces a direction reversal need be addressed in planning.
We narrate the problem and may highlight a possible formalisation.
We shall only hint at the below problems and their formal solution:
SOFTWARE DEVELOPMENT: FROM DOMAINS TO SOFTWARE
We overview domain requirements, interface requirements and machine requirements issues and indicate how to create domain requirements from domain descriptions using a number of domain-to-requirements operations: projection, determination, instantiation, extension and fitting.
We very briefly indicate how to bridge the development from domain description of a simple time table concept via requirements to a component-based distributed and concurrent client/server computing system.
We indicate essential issues in domain models for:
And we close by discussing, with participants, modalities of creating and propagating domain theories.
PETRI NETS
MESSAGE SEQUENCE CHARTS (MSCS)
COMMUNICATING TRANSACTION PROCESSES (CTPS)
All lecture slides will be made available electronically, on day of lecture. Usually such that one can print eight slides to an A4 page.
Dines Bjørner
National University of Singapore