Dines Bjørner
June 18, 2003A ``Grand Challenge'':
Unifying Theories of Formal Methods
- Integrating Formal Methods -
CSE: Computer Science and Engineering
IMM: Informatics and Mathematical Modelling
Building 322, Richard Petersens Plads
DTU: Technical University of Denmark
DK-2800 Kgs.Lyngby, Denmark
E-Mail: db@imm.dtu.dk, URL: www.imm.dtu.dk/~db
| To be written |
| To be written |
| To be written |
Several Integrating Formal Methods (IFM) conferences have been held. Proceedings have been published in Springer-Verlag's Lecture Notes in Computer Scxience Series:
Call for Papers:
Formal methods have been established as the rigorous engineering methodology for the system development. Applying formal methods to a large and complex system development often requires the modelling of different aspects of such a system. For instance, complex systems (such as integrated avionics systems, engine control software) can involve functional and timing requirements that must be eventually implemented as executing code on a communicating distributed topology.
Recent research on multi-paradigmed approaches has recognised the need to combine different formal viewpoints on the same system. Process algebras have been devised with algebraic data types (e.g. (E-)LOTOS, CRL) and more recently a number of approaches have been proposed that combine or extend established model-based techniques with behavioural formalisms. Examples include: MTCCS, TLA, Action Systems, B with modal extensions, RSL, Z (and Object-Z) with CSP, Timed Z, Z and CCS, RTL+Z.
Programme Committee:
K. Araki - Kyushu U., Japan (Chair) S. Hayashi - Kobe U., Japan S. Liu - Hiroshima CU., Japan G. Smith - U. of Queensland, Australia C. Fischer - U. of Oldenburg, Germany A. Evans - U. of York, UK J. Derrick - U. of Kent, UK J.S. Dong - NU. of Singapore, Singapore J. Woodcock - U. of Oxford, UK A. Galloway - U. of York, UK (Co-Chair) H. Habrias - U. of Nantes, France H. Toetenel - Delft UT., Nederlands D. Mery - U. of Nancy, France J. Bowen - U. of Reading, UK W. J. Stoddart - U. of Teesside, UK C. Fidge - U. of Queensland, Australia K. Taguchi - Kyushu U., Japan (Co-Chair) M. Hinchey - U. of Nebraska-Omaha, USA (U. of Limerick, Ireland) J-R. Abrial - Consultant, France J. Sinclair - U. of Warwick, UK J. McDermid - U. of York, UK H. Lin - Chinese Academy of Sciences, China C. George - United Nations U., Macau
Call for Papers:
Applying formal methods may involve the modelling of different aspects of a system that are expressed through different paradigms. This motivates us to research the combination of different viewpoints of a system, either by the creation of hybrid notations, by extending existing notations, by translating between notations, or by incorporating a wider perspective by innovative use of an existing notation.
The integration of formal methods promises great benifits for systems modelling and software development. Whichever approach is taken, significant issues can arise in areas such as semantic integration, the tractability of our notations, the integration of tool support, the integration of proof systems, consistency and completeness. Issues arise equally in our conceptualisation of systems at different levels of abstraction and the development of these conceptualisations through the process of refinement.
The stated theme of IFM99 was the integration of state based and behavioural formalisms. For IFM2000 this has been widened to include all aspects pertaining to the integration of formal methods and formal notations.
Programme Committee:
Keijiro Araki, Univ of Kyushu, Japan Didier Bert, Univ of Grenoble, France Egon Boerger, Univ of Pisa, Italy Jonathan Bowen, Southbank University, London, UK Micheal Butler, Univ of Southampton, UK Jim Davies, Oxford University, UK John Derrick, Univ of Kent, UK Heiko Doerr, Daimler Chrysler, Germany Jin Song Dong, National Univ of Singapore Clemens Fischer, Univ of Oldenburg, Germany John Fitzgerald, Univ of Newcastle, UK Andy Galloway, Univ of York, UK Chris George, United Nations University, Macao Wolfgang Grieskamp, Technical Univ of Berlin, Germany Henri Habrias, Univ of Nantes, France Susumu Hayashi, Kobe University, Japan Maritta Heisel, Univ of Magdeburg, Germany Mike Hinchey, Univ of Omaha, USA Bernd Krieg-Brueckner, Univ of Bremen, Germany Michel Lemoine, ONERA, Toulouse, France Shaoying Liu, Hiroshima City Univ, Japan John McDermid, Univ of York, UK Dominique Mery, LORIA, France Thomas Santen, Technical Univ of Berlin, Germany Steve Schneider, Royal Holloway, UK Wolfram Schulte, Microsoft Research, USA Jane Sinclair, Warwick University, UK Graeme Smith, Software Verification Centre, Queensland, Australia Bill Stoddart, University of Teesside, UK Kenji Taguchi, Uppsala University. Sweden W J (Hans) Toetenel, University of Delft, Holland Heike Wehrheim, University of Oldenburg, Germany
Call for Papers:
Applying formal methods may involve the modeling of different aspects of a system that are expressed through different paradigms. This motivates us to research the combination of different viewpoints upon a system, either by the creation of hybrid notations, by extending existing notations, by translating between notations, or by incorporating a wider perspective by innovative use of an existing notation.
The integration of formal methods promises great benefits for systems modeling and software development. Whichever approach is taken, significant issues can arise in areas such as semantic integration, the tractability of our notations, the integration of tool support, the integration of proof systems, consistency and completeness. Issues arise equally in our conceptualization of systems at different levels of abstraction and the development of these conceptualizations through the process of refinement.
The stated theme of IFM99 was the integration of state based and behavioral formalisms. For IFM2000 this has been widened to include all aspects pertaining to the integration of formal methods and formal notations. The goal of IFM2002 is to further and deeper explore the themes stated for its predecessors. Moreover, IFM2002 intends to build upon them and explore the existent and the possible relations between formal methods and the new industrial standard language for software design, the Unified Modeling Language (UML).
Programme Committee:
Didier Bert, Institute IMAG, Grenoble, France Jonathan Bowen, South Bank University, London, UK Michael Butler, University of Southampton, UK Jim Davies, Oxford University, UK John Derrick, University of Kent, UK Jin Song Dong, National University of Singapore John Fitzgerald, Transitive Technologies Ltd, Manchester, UK Andrew Galloway, University of York, UK Chris George, United Nations University, Macao Wolfgang Grieskamp, Microsoft Research, Redmond, US Henri Habrias, University of Nantes, France Susumu Hayashi, Kobe University, Japan Maritta Heisel, University of Magdeburg, Germany Michel Lemoine, ONERA, Toulouse, France Shaoying Liu, Hosei University, Tokyo, Japan Dominique Mery, LORIA, France Luigia Petre, Turku Centre for Computer Science, Finland Thomas Santen, Technical University of Berlin, Germany Steve Schneider, Royal Holloway, University of London, UK Wolfram Schulte, Microsoft Research, Redmond, US Kaisa Sere, AAbo Akademi University, Turku, Finland Jane Sinclair, Warwick University, UK Graeme Smith, Software Verification Centre, Queensland, Australia Bill Stoddart, University of Teesside, UK Kenji Taguchi, Uppsala University, Sweden W J (Hans) Toetenel, University of Delft, Holland Heike Wehrheim, University of Oldenburg, Germany Jim Woodcook, Oxford University, UK
Call for Papers:
Applying formal methods may involve the modelling of different aspects of a system that are expressed through different paradigms. This motivates us to research the combination of different viewpoints upon a system, either by the creation of hybrid notations, by extending existing notations, by translating between notations, or by incorporating a wider perspective by innovative use of an existing notation.
The integration of formal methods promises great benefits for systems modelling and software development. Whichever approach is taken, significant issues can arise in areas such as semantic integration, the tractability of notations, the integration of tool support, the integration of proof systems, consistency and completeness. Issues arise equally in our modelling of systems at different levels of abstraction and the development of these models through the process of refinement.
The scope of IFM2004 includes all aspects of integration of different notations, paradigms, and tools, including integration of state-based and behavioural formalisms, and the formal strengthening of informal notations (e.g., UML). Special sessions are planned on the themes of Unifying Theories of Programming as well as Testing, and submissions for these are welcomed.
The necessity of tool support for formal methods is widely accepted. However, much existing tool support fails to exploit the advantages that formality brings. This year's IFM is therefore particularly interested in how integrating formal methods can facilitate tool support for the development process, either by integrating tools or exploiting the particular languages combined.
The conference also seeks and welcomes contributions in related areas such as: hybrid systems, the embedding of one formalism within another, and the integration of formal methods with informal or semi-formal diagrammatic notations and structuring techniques.
Programme Committee:
Didier Bert, Institute IMAG, Grenoble, France Eerke Boiten, University of Kent, UK Jonathan Bowen, South Bank University, London, UK Michael Butler, University of Southampton, UK Paul Curzon, Middlesex University, London, UK. Jim Davies, University of Oxford, UK John Derrick, University of Kent, UK Jin Song Dong, National University of Singapore John Fitzgerald, Transitive Technologies Ltd, Manchester, UK Andrew Galloway, University of York, UK Chris George, United Nations University, Macau Wolfgang Grieskamp, Microsoft Research, Redmond, US Henri Habrias, University of Nantes, France Susumu Hayashi, Kobe University, Japan Maritta Heisel, University of Magdeburg, Germany Michel Lemoine, ONERA, Toulouse, France Shaoying Liu, Hosei University, Tokyo, Japan Dominique Mery, LORIA, France Luigia Petre, Turku Centre for Computer Science, Finland Judi Romijn, Eindhoven University of Technology, NL Thomas Santen, Technical University of Berlin, Germany Steve Schneider, Royal Holloway, University of London, UK Wolfram Schulte, Microsoft Research, Redmond, US Kaisa Sere, Abo Akademi University, Turku, Finland Jane Sinclair, University of Warwick, UK Graeme Smith, Software Verification Research Centre, Queensland, Australia Bill Stoddart, University of Teesside, UK Kenji Taguchi, Uppsala University, Sweden W J (Hans) Toetenel, University of Delft, Holland Heike Wehrheim, University of Oldenburg, Germany Kirsten Winter, Software Verification Research Centre, Queensland, Australia Jim Woodcock, University of Kent, UK
This section can be skipped in any reading. It presents a set of characterisations of the fields of computer & computing science, domain, requirements and software engineering, and the concepts of domain, requirements, model and theory such as the present author of the current document understands these fields. As such the section ``signals'' the didactics ``from'' which the present author of the current document understands the challenge being put forward.
We ``risk'' some characterisations:
By a(n application) domain we understand an area of (possibly computing supportable) human activity -- such as a bank and its interfaces to its customers, other banks, regulatory agencies, etc.
We are to understand, in the ``narrow'' context of the term `domain', such a domain void of any reference to computing not already in the domain. That is: If the purpose of our trying to understand a domain is - later on - to install computing /and communication) in support of activities of the domain, then (requirements to, let alone software of) that future computing (and communications) is not to be mentioned in the domain.
This domain is a major infrastructure component, ie., is a socio-economically driving force of a country, or a region, in securing that area's social and economic structure and well-being.
To `The Financial Service Industry' we ``count'' the sets of such enterprises as banks, insurance companies, securities institutions (trader, brokers and exchanges), venture capatial firms, etc., as well as the country's and/or region's regulatory agencies. We also ``count'' all the clients of these enterprises, including politicians.
To describe `The Financial Service Industry', to us, means to describe all those enterprises, agencies, clients, etc., as well as their interaction. To wit: The opening and closing of accounts, as well as all the varieties of transactions ``against'' accounts: Deposits, withdrawals, transfers, etc.
This domain is a major infrastructure component, ie., is a socio-economically driving force of a country, or a region, in securing that area's social and economic structure and well-being.
To `Transportation & Logistics' we ``count'' the sets of such enterprises as railway (bus, shipping, air) infrastructure owners (eg., the railway net (resp. roadnet, airport, and harbour) owners), railway (bus terminal and road net [toll way etc.], harbour and canal, airport and air traffic control) infrastructure operators (operating the nets: Lines and stations, signalling, etc., resp. bus deports and toll ways, harbours and canals, airport), train (bus, shipping, airport and air traffic) service providers (on shared transport nets), regulatory agencies, clients (ie., passengers, companies wishing to transport freight, etc.), providers of services to the above (equipment manufacturers, net (bus depot and road net, harbour and canal, aiport and air traffic control center) construction firms, travel agencies, etc.), and especially logistics firms (which offer services to freight customers: Arranging composite transfer of goods via combinations of rail (freight train), road (truck), ship (boat), and air (cargo).
To describe `Transportation & Logistics' means to describe all those enterprises, agencies, clients, etc., as well as their interaction.
Just exemplifying for railways we briefly mention the entities, functions and behaviours of the specific domain: (1) The net (lines and stations), (2) the trains, (3) the net operations (signalling, stations, etc.), (4) the despatch: monitoring and control of trains, (5) the handling of passengers and freight, (6) the planning, development and phasing-in of new lines and stations and the phasing out of lines and stations, of new train services, (7) the scheduling and allocation of: (7.i) time-tables, (7.ii) rostering of train crews, (7.iii) the composition and decomposition of trains, (7.iv) train maintenance, etc., etc.,
Similar outlines can be given for bus transport, for shipping, and for air transport.
This domain is a major infrastructure component, ie., is a socio-economically driving force of a country, or a region, in securing that area's social and economic structure and well-being.
To `Health-Care' we count such enterprises as (1) healthy and sick people (ie., potential or actual patients), (2) private (family doctor) physicians, ie., general practitioners and specialist medical doctors, (3) community nurses, (4) hospitals, (5) ambulance services, (6) clinics (convalescence and special treatment), (7) pharmacists, (8) health insurance companies, (9) interfaces to the pharmaceutical industry, (10) the national board of health, (11) ministry of health, etc.
To describe `Health-Care', to us, means to describe all those enterprises, agencies, clients, etc., as well as their interaction. To wit: Patient visits to family physicians, pharmacies, clinics, and hospitals, the actual functions performed at these places: analyses, diagnostics, treatment and treatment advice (incl. medication and their prescription), check-up on results of treatments, etc., MR and CT scanning, surgical operations, etc. Patient interaction with health insurance institutions: Registration, premium payments, claims, etc. Medical doctor, community nurse, clinic, pharmacy and hospital reportings to health authorities, etc.
By ``The Market'' -- for goods (merchandise) and services we mean the aggregation of government agencies (G), businesses (B) and citizens (C). Here government institutions include such as social welfare, excises & tax, etc.; businesses include producers, wholesalers and retailers -- seen from the point of view of their interaction, and retailer interaction with consumers (ie., citizens). And citizens cover all of us in our relations to government agencies, businesses (usually retailers, agents on behalf of these, and brokers between them and citizens), and to other citizens (in for example citizen associations (societies), etc.).
To describe ``The Market'' , to us, means to describe, from the point of view of the G2G, G2B, G2C, B2G, B2B, B2C, C2G, C2B, and C2C interactions, all those interacting ``players'' belonging the sets G, B and C. For example, the C2B (where B is a retailer) interactions are for example: (C) Inquire as to whether a retailer has a certain merchandise, price, delivery time, etc., (B) acknowledge such an inquiry, (C) order merchandise, (B) acknowledge or declien an order, (B) deliver ordered merchandise, (C) accept or reject delivery, (B) invoice delivery, (C) pay invoice, (C) return merchandise for repair or replacement, etc.
Similar such interactions can be identified for each of the remaining G2G, G2B, G2C, B2G, B2B, B2C, C2G, and C2C.
In understanding a domain it seems advicable that one decomposed and ``serialises'' one's understanding into the understanding of a number of related facets. A facet is a way of viewing a thing, in this case `the domain'. We suggest to at least view a domain from the point-of-view of the folowing facets.
By the intrinsice of a domain we understand those properties, of a domain, which any other facet/view is based on. That is, each of the next facets to be treated all have their treatment, their understanding, their description, depend on there first being established an understanding of the very basics, the intrinsics.
Example: We pursue the example of railways: It seems that whoever you are, a railway owner, a net operator, a train operator, a passenger, etc., (1) the net: the fact that there are stations and that some of these are ``non-stop'' connected by (rail) lines, and (2) the trains, running on the net, along lines and between stations, that that is part of the intrinsics of a railway system.
By the supporting technologies of a domain we understand those facilities, of a domain, other than human actors, which support operations of the domain.
Example: In ``ye olde days of railways'', switches (turn-outs, points, etc.) - units along the rail where a route through the rail units merges or diverges - were handled by humans throwing, by the shear force of their muscles, these switches. Later the switches became operated by mechanical means: From a cabin tower, levers, mechanical momentum amplifiers and wires connected, sometimes hundreds of feet away, to the switches. Yet later, to illustrate a thrid kind of supporting technology, the mmechanics was extended into electro-mechanics. Most recently we find that switches are operated in groups, involving also significant electronics, and, ever more recently, with these operations being controlled by computers.
All of the above exemplified several (``generations'' of) supporting technologies. In current domains we shall today find that several such supporting technologies co-exists. And have to be understood.
By domain management & organisation we understand a structured decomposition of the work of domain staff into usually a hierarchical or a matrix structured organisation where ``lines of command & reporting'' flow along the hierarchical tree or the horisontal/vertical grid of the matrix organisation: Where managers formulate policies, rules & regulations, and issue directives to ``levels below them'' in the structure, where they respond to ``alerts'' and reports from''below them'' in the structure, and where they ``alert'' and report to other managers, or the board, ``above them'' in that structure.
Example: In China, along the rail lines, from station to station, the reschedulng of trains - due to late or early trains - involves certain procedures (ie., management) and certain communications with colleagues in neigbouring stations (ie., organisation), before a proposed new train schedule can be ``universally'' adopted.
By domaon rules & regulations we understand two sets of ``laws'': One set, the regulations, which specify expectations of ``acceptable'' behaviour of equipment and humans; another set, the rules, which stipulate what corrective actions, against equipment, operations, and/or staff, are to be taken in case rules are not fulfilled.
Example: In China, for reasons we shall not endeavour to explain, train traffic into and out of railway stations are expected to satisfy the following rule: In any two minute interval (ie., period), at most one train is allowed to either enter or to leave a(ny) station. The ``pairing'' regulations state how to achieve this, and also stipulates administrative (ie., ``punitive'') measures to be enacted if equipments and/or humans fail to satisfy the rule.
Humans, whether staff of, or clients (customers) or others related to the enterprise, behave either (1) diligently: despatch their work within the enterprise with careful regards to rules & regulations (whether these are explicitly enunciated or are tactily understod), or they behave (2) sloppily, with casual, arrogant or indolent respect for such expected behaviours, or they behave (3) negligently, with somewhat recalsitrant (obstinately defiant of authority or restraint), or they behave (4) outright criminally, explicitly, and on purpose, with a specific, say destructive intent in mind, going against rules & regulations.
To understand a domain is also to understand the possibilities of staff and clients (etc.) to create harmony or havoc.
A doman is also characterised by its stake-holders. These are the various people and institutions ``united'' in separate interest groups - that potentially may have different, possibly inconsistent, either reconcilable or ir-reconcilable (ie., conflicting) views of (on) the domain.
An important aspect of domain identification and construction is to identify, record, and communicate, during the construction process with suitably selected members of each of the selected stake-holder groups. They are the ones from whom to acquire the appropriate domain knowledge, and they are the ones with whom to validate the emerging domain models.
Typically, for a production company one can identify the following stake-holder groups: (i) Oweners, (ii) executive management, (iii) middle management, (iv) ``floor'', ie., ``lowest'' level management, (v) workers (in administration, sales, marketing, design, research, production, etc.), (vi) clients (who buy the products), (vii) suppliers (of parts and materials, power (electricity), water, IT, etc.), (vii) consumer/client organisations, (viii) regulatory agencies, (ix) politicians (who ``meddle'' in well-nigh every matter), (x) neighbours of the production company's sites, (xi) the media (newpapers, radio, TV), and (xii) the general public (``man on the street'').
A model is only acceptable if it reflects the views of each and all of these stake-holder groups. Two (or more) such views may be inconsistently represented in a model (under development) -- in which case one has to inquire whether that inconsistence is due to an oversight on behalf either of the developers (then it can be remedied by them alone), or on behalf of the two (or more) stake-holder groups (in which case some mutual clarification process is needed); or that inconsistence may be due to an inherent conflict between stake-holder groups. In the latter case domain management must be brought in to reconcile the inconsistency.
But, in any case, we can expect a domain model to consist of of a set of judiciously harmonised (integrated, unified) formal models.
By a model we mean a description, both in plain natural (cum national) language, and in formal terms: In any combinations of mathematics and various, one or more, formal specification languages.
A model is not the reality of the domain, only a reflection of it.
Models involve iconic, analogic and analytic facets, are either prescriptive or descriptive, or combinations thereof, and models may also involve variations or combinations of intensionality and exensionality (``white'' versus ``black'' box views).
Models are constructed in order (a) to understand that which is being modelled [ie., the domain], (b) to inform others about that ``thing'', (c) to perform predications about the behaviour of the ``real thing'' (based on computations over the, ie., ``its'' model), (d) to implement computing support for activities of the domain, (e) to perform business process reengineering of operations (human or otherwise) of the domain, (f) or other.
A model usually consists of different types of document parts:
Informative document parts, as the term says, inform: Presents a (1) reason for why the model is constructed, its rationale so-to-speak, that is: The (prior) needs for and (subsequent [planned]) uses of the model (that is: The ``customers''); (2) lists who is constructing, or has constructed, the model (the partners); (3) a budget for and accounts of economic aspects of constructing the models (imcl. project time & resource plans, etc.); and possibly other information.
There usually are four kinds of descriptive document parts:
When initially starting work on a model the developer cum researcher
rough sketches. Rough sketches serve to
form
concepts
based on (ie., around) which the model is eventually
expressed. The concepts are abstractions of ``actual world''
phenomena.
Along the road of model development specific terms of the domain are identified and defined. And these terms eventually enter into some ontology for the domain.
Based on clear concepts, and evolving terminology and ontology, the developer can now formulate, in precise, but informal, natural and professional (term) language a description of the entities, functions and behaviours (events, interactions and processes) of the domain.
Usually the narrative goes hand-in-hand with a set of one or, usually more, formalisations, ie., formal specifications. Usually one formalism does not suffice. It appears that no one specification language can equally elegantly and expressible model all domain attrubutes, facets and stake-holder perspectives. One is therefore forced to use several formalisms.
We alphabetically mention a few formalisms: ASM (Abstract-State Machines) (since early 1990s), B (``Bourbaki'') (since early 1990s), CASL (Common Algebraic Specification Language (since 1997), CafeOBJ (since 1997), DC (Duration Calculi) (since 1990), ITL (Interval Temporal Logic) (since late 1980s), RAISE (Rigorous Approach to Industrial Software Engineering) (since 1986), TLA+ (Temporal Logic of Actions + Set Theory) (since mid 1990s), Petri Nets (since 1963), CSP (since 1978), Statecharts (since mid 1980s), pi-Calculus (of Mobile Processes) (since late 1990s), VDM (Vienna Development Method) (since 1973), and Z (``Zermelo'') (snce 1980).
We refer to Recent Trends in Formal Techniques and Tools for Software Development for Transportation Applications - A Survey and TLA+ as sources for references to the above-listed approaches to formal specifications.
It is to be hoped that a set of theories can be brought about, theories which ``unify'' pair- or triple-wise combinations of the above and other formal method approaches. We refer to Unifying Theories of Formal Methods - Integrating Formal Methods
Analytic document parts arise as the result of analysing descriptive document parts.
There usually are four kinds of analytic document parts:
When models are formalised, then it is possible to derive properties from the model that are believed to be properties of the domain (being modelled). The set of axioms and inference rules upon which the formal description of the models are based, as well as the possible lemmas, propostions and theorems derived from those axioms and deduction rules, form a theory.
See the last two entries itemised above.
Computing systems engineering, to us, is concerned with the development of hardware + software solutions to problems. As such it involves software engineering and hardware engineering and their interplay, usually referred to as co-design. We shall only further characterise software engineering.
Software engineering, to us, is a convergence, a fusion, between domain engineering, requirements engineering and software design - in the context of computer systems engineering, ie., with due considerations, also, of interfaces to hardware.
Domain engineering - in the light of the above, to us - is concerned with the analysis and syntehsis (ie., construction), ie., development of domain models (incl., domain theories) - thus with due respect to all relevant stake-holder groups.
Requirements engineering, to us, is concerned with the development of requirements. At this place in our presentation we shall not mention the relevant issues of requirements acquisition and validation, but focus exclusively on the structure of a (set of) requirements models.
But first we need a crucial definitions:
We postulate that there are basically three requirements document parts, either presented, in the model, separately, or intertwined, but in a clearly recognisable fashion:
Hence:
Wirhnin `Domain Requirements' we can identify a number of principles and techniques that huide us in their construction and expression. We mention some:
Usually a domain model consists of very many specfications and covers a large ``terrain''. For any specific requirements only a fraction of the domain is relevant. Projection is like an algebraic operation which ``narrows'' the domain model into those parts of relevance to the requirements.
Usually a domain behaviour is non-deterministic and so are, therefore, its models. Determination is like an algebraic operation which removes undesired non-determinisms.
Sometimes domains do not admit certain kinds of functionalities: They are simply not (humanly or, up to this moment, technologically) feasible. With the advent of computing and communication some such functionalities are now made feasible. Extension is like an algebraic operation which extends, basically the domain - but phrased, usually, within the requirements.
Normally a domain model generically covers sets of domain instances: Many different railway systems, or may different health-care systems, etc. Instantiation is like an algebraic operation which binds certain loosely specified properties of a generic doman model to specific such properties. Examples could be: (1) A specific set of train despatch rules & regulations - although even these may be left ``programmable''; or (2) a specific kind of railway net topology, topologically bound by certain kinds of local practices.
Normally required software is to work together with pre-existing hardware and software sub-systems. And although basically a machine requirements (ie., a platform) issue, we consider fitting like an algebraic operation which concretises certain domain properties in certain directions as biased by the chosen pre-existing hardware and software sub-systems.
Invariantly the required software, before installation, need be initialised to some basic data, ie., an initial database need be established, or an existing need be migrated. Initialisation binds certain facets of domain configurations to to static, ie., contextual ``values'', while others are initially set to some dynamically changing initial ``values''. Initialisation requirements further prescribe how the configuration contexts and states may be kept ``up-to-date''.
By software design we understand the derivation, from requirements, of provably correct software.
The design process can be structured, for example, as follows:
Usually a set of requirements models give little hint as to the overall structure of the software design: A computable structure, called the software architecture, must be set up. Depending on machine requirements issues the developer may be forced to consider such issues before domain, or before interface requirements concerns.
By a component we understand a set of modules such that the coherence between the modules in the component set (c) is high, or higher than any other set of modules (c') overlapping with c. Usually a component is determined by either considerations of domain requirements, or considerations of machine requirements, or considerations of interface requirements.
The ``etcetera'' covers over such things as module design and code development.
By informatics we shall understand the confluence of mathematics, computer science cum programming methodology, and applications.
Informatics relate to IT as biology relates to bio technology, that is ``tangentially''. One embodies the other. Informatics is basically a science and a practice which builds on mathematics (linguistics and philosophy). IT builds on the natural sciences.
IT is characterised by material issues of quantity: Faster, smaller volume, cheaper, large capacity, etc. Informatics can be characterised by issues of intellectual quality: Better ``fit'', more pleasing, elegant, etc.
IT, in a sense, represents a universe of material quantity. Informatics one of intellectual quality.
| Here we plan to give reference to a great number of papers &c. |
We refer to the following MSc student project report:
Event Condition, Place Transition and Coloured Petri Nets are explained and formalised in RSL (the RAISE Specification Language ). So are Message Sequence Charts and Statecharts. Then three different, non-trivial examples are expressed in respectively Coloured Petri Nets, Message Sequence Charts and Statecharts. Each of these three examples are then re-stated in RSL.
In Christian Krog Madsen's continued work it is expected that he will
(1) define translations from
Coloured Petri Nets
(CPNs)
into
RSL,
from
Live Sequence Charts (LSCs)
into
Timed RSL,
and from
Statecharts
(SCs)
into
RSL;
(2) then be concerned with these
translations satisfying
some semantics relations or other; (3) investigating under which
conditions reverse translations can occur for certain
RSL
specifications into respective
CPNs, LSCs
or
SCs.
| To be written |
| To be written |
| To be written |
In the companion ``Grand Challenge'' for Domain
Models & Theories of Transportation Systems &
Logistics
an assumption was tacitly made:
That the intrinsics
of the domain was basically invariant:
That indeed, the core parts of a domain model had a stable ``target'' to model.
For the area of `Unifying Theories of Formal Methods - Integrating Formal Methods' the very basics of the problem has been captured in:
but that basis is too abstract. A ``Grand Challenge'' for `Unifying Theories of Formal Methods - Integrating Formal Methods', must, we take as a dogma, start on the basis of existing formal techniques. Some such were tentatively listed in A List of Formal Techniques and Tools. But any such list is temporary: Some of the techniques listed above have endured 30 years (ie., VDM), others have basically been extended (more or less beyond comparison, viz.: LCS and MSC).
Thus the challenge can
not only
be that of finding suitable pairings (or
triplings, etc.) of existing formal techniques and provide
``unifications'' cum ``integrations'' for these ``groupings''.
Instead, it is believed, it must
also
be that of providing
such relations
whenever
a new formal notational tool and its
techniques are being put forward.
| To be written |
| To be written |
| To be written |
The current author of this document presently (ie., June 18, 2003) thinks that it will take at least 10 years, probably more realistically up towards 20 years, before a reasonably complete ``Unification'' will have been both established and generally accepted.
The current author of this document presently (ie., June 18, 2003) expects the following to hold for at least an initial 4-5 years of a ``Grandest Challenge'' project:
| To be written |
| To be written |
The current author of the present document has the following, somewhat provocative, opinions:
It may be that some of the 5-10-20 worldwide groups are locally funded. No comments.
Otherwise it should be curtailed.
And: If they are worth anything, that ``worth'' should be of such a nature, and so obvious, that local, say software industry, and/or regional, public, say EU, funding agencies wishes to fund - ie., by themselves ought offer to ``ride the band-waggon'', to be associated with an emerging success story.
/home/db/colognet/web/utopia.tex
This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.47)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
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 6 utopia
The translation was initiated by on 2003-06-18