Software Blueprints : Lightweight Uses of Logic in Conceptual Modelling

by Robertson, David; Agusti, Jaume

• ISBN13: 9780201398199
• ISBN10: 0201398192
• Format: Hardcover
• Copyright: 1999-08-01
• Publisher: Addison-Wesley Professional

Summary

Conceptual models are descriptions of our ideas about a problem, used to shape the implementation of a solution to it. Everyone who builds complex information systems uses such models - be they requirements analysts, knowledge modellers or software designers - but understanding of the pragmatics of model design tends to be informal and parochial. Lightweight uses of logic can add precision without destroying the intuitions we use to interpret our descriptions. Computing with logic allows us to make use of this precision in providing automated support tools. Modern information scientists need to know what these methods are for and may need to build their own. This book gives you a place to begin. Where do you start when building models in a precise language like logic? One way is by following standard paradigms for design and adapting these to your needs. Some of these come from an analysis of existing informal notations. Others are from within logic itself. We take you through a sample of these, from more commonplace styles of formal modelling to non-standard methods such as techniques editing and argumentation. Each of these provides a window onto broader areas of applied logic and gives you a basis for adapting the method to your own needs.

Author Biography

David Robertson is a lecturer in the Division of Informatics at Edinburgh, where he leads the Software Systems and Processes Group. His research (currently supported by an advanced fellowship from the UK Engineering and Physical Sciences Research Council) is primarily on the use of computational logic to support the design and analysis of complex systems and problem descriptions. Jaume Agusti is head of the Department of Formal Methods in the Institut d'Investigaci en Intelligencia Artifical (CSIC) at Bellaterra (Barcelona), where he leads the Computational Logic Group. His research is primarily on the refinement of formal requirements and high-level specifications into computational models of complex problems.

Table of Contents

Foreword	xiii
Preface	xv
How to read this book	xv
Acknowledgements	xvii
Introduction	1	(10)
A dream	1	(1)
Reality	2	(1)
Our corner of the problem	2	(1)
What you can learn from this book	3	(1)
The way we view conceptual modelling	4	(7)
Models of problems are not specifications of solutions	4	(1)
What we require of conceptual models	4	(2)
Lightweight use of formality	6	(1)
Our use of logic	7	(1)
The need for eclecticism	7	(4)
Models in a design lifecycle	11	(24)
Requirements analysis	12	(5)
Choice of representational paradigms	17	(2)
Communication between divisions	17	(1)
Decision procedures within divisions	18	(1)
Model construction	19	(5)
Communication between divisions	19	(2)
Decision procedures within divisions	21	(3)
Validation and verification	24	(6)
Validation by analysing potential behaviours	24	(5)
Using our requirements to justify design decisions	29	(1)
Issues raised by our example	30	(5)
Argumentation networks	32	(1)
More extensive examples using operator models	32	(1)
Conceptual models in knowledge engineering	32	(1)
Model checking	33	(1)
Exercises	34	(1)
Logic as a modelling language	35	(32)
Logics as frameworks for argument	35	(4)
The boundary problem	39	(4)
The search problem	43	(1)
Proof strategies	44	(2)
Describing proof strategies formally	46	(1)
Distinguishing proof rules from selection strategies	47	(2)
Knowing when two terms unify	49	(2)
The closed world assumption	51	(1)
Non-deductive patterns of inference	52	(4)
Abduction	53	(1)
Induction	54	(2)
Ontologies	56	(3)
Some properties of logical languages	59	(4)
Logical consequence	59	(1)
Correctness and completeness	60	(1)
Decidability	61	(1)
Correctness and completeness of arguments	62	(1)
Further reading	63	(4)
Exercises	63	(4)
Communication	67	(24)
From domains to formal languages	68	(13)
An entity relationship diagram	69	(4)
A BSDM entity diagram	73	(2)
Lessons from the comparative analysis	75	(1)
Building an early model	76	(3)
Checking the consistency of the model	79	(1)
Lessons learned from more detailed modelling	80	(1)
From formal languages to domains	81	(6)
Visual formal expressions	81	(4)
Formal problem description by means of diagrams	85	(2)
The correspondence between logic and diagrams	87	(4)
Exercises	88	(3)
Re-use of paradigms: parameterisable components	91	(24)
Worldwide web site generation	93	(4)
Problem description language (research group)	95	(1)
Parameterisable components (site pages)	95	(1)
Parameterisation system (simple instantiation)	96	(1)
Design generated (web site)	96	(1)
Rapid domain-specific model generation	97	(6)
Design generated (animal population model)	98	(2)
Parameterisable components (model fragments)	100	(1)
Problem description language (ecological conditions)	101	(1)
Parameterisation system (constrained generation)	102	(1)
Design endorsements	103	(7)
Problem description language (domain notations)	103	(1)
Design generated (shutdown specification)	104	(2)
Parameterisable components (shutdown segments)	106	(1)
Parameterisation system (design endorsement)	106	(4)
Costs and benefits	110	(2)
Further reading	112	(3)
Exercises	113	(2)
Design processes inspired by formal methods	115	(20)
Constructing definitions by slices	116	(6)
Skeletons and additions	117	(1)
A techniques editor at work	118	(4)
Re-using part of an earlier definition	122	(2)
Using design histories when combining definitions	124	(3)
Issues raised by our example	127	(8)
Structured formal definition and transformation	127	(1)
Stripping structure from predicates	128	(1)
Case-based reasoning	128	(4)
Exercises	132	(3)
Argumentation	135	(22)
Reasoning about sources of uncertainty	135	(8)
Reconstructing the model in logic	137	(3)
Reasoning about uncertainty in the model	140	(3)
Justifying design decisions	143	(5)
Data describing reserve sites	145	(1)
Formal requirements guidelines	145	(2)
Interactively constructing justifications	147	(1)
Accommodating the dynamics of argument in logic	148	(5)
An example of defeasible argumentation	149	(3)
An abstract argumentation framework	152	(1)
Further reading	153	(4)
Exercises	155	(2)
Temporal reasoning	157	(22)
Reasoning with temporal intervals	157	(4)
Modal temporal logic	161	(6)
An example using a `ticking clock' time sequence	161	(2)
A modal temporal logic for our example	163	(1)
Proofs in modal temporal logic	164	(2)
Other kinds of modal operators	166	(1)
Reasoning with temporal constraints	167	(8)
Determining when properties hold	170	(1)
Temporal constraint networks	171	(4)
Further reading	175	(4)
Exercises	176	(3)
Syntax, semantics and pragmatics	179	(6)
Syntax	179	(1)
Semantics	180	(3)
Linguistic interpretation	181	(1)
A formal semantics for each modelling language	181	(1)
A formal semantics for all modelling languages	182	(1)
Semantics of a family of models within a lifecycle	182	(1)
Pragmatics	183	(2)
Conclusion	185	(6)
A summary of our main arguments	186	(2)
Lightweight tools	188	(1)
Closing remarks	188	(3)
Appendix A Glossary	191	(4)
Appendix B Syntax of expressions	195	(2)
Appendix C Answers to exercises	197	(10)
References	207	(10)
Index	217

Excerpts

We wrote this book for a variety of reasons: to satisfy our curiosity; to challenge some existing preconceptions; to bring together areas of work which are traditionally separated; and for our own enjoyment. System design, in the large, involves many stages of description prior to the specification of the system itself. Opinions differ about what theses stages should be and surprisingly little is known about how they fit together - yet somehow (with widely differing degrees of success) groups of people manage to construct complex systems using all sorts of intermediate descriptions to help them understand their problem. We are curious about how this process works and whether parts of it can be understood more precisely. Our precision tools are logics, which too many people associate with an ‘all or nothing' attitude to formal description. Faced with the choice of ‘all' or the effort of understanding a comprehensive formal specification method of having ‘nothing' to do with logic, most practising designers have chosen ‘nothing'. It need not be so. We shall demonstrate that judicious use of logic in simple ways at strategic points in the description of a problem can be helpful, without requiring revolutionary change in work practices. We shall also demonstrate that appropriate use of logic makes it possible to introduce inference methods from the artificial intelligence and logic programming communities. This has a practical aim - to extend the armoury of designers - but a larger motivation is to emphasise the synergy between these areas of research. This book is also a blend of theoretical and applied research, reflecting the different backgrounds of the two authors. Much of our enjoyment has been in reconciling opinions shaped by these different cultures. How to read this book The aim of this book is to explain how systems of formal representation and automated reasoning may be applied to early stages of software design. Although much of the cost of design stems form difficulties at this level, this is new territory for many of those concerned with precision in design and requires a non-traditional view of what it means to build such systems. Traditionally, logics are used when we have a precisely understood problem. The goal is then to choose the most elegant mathematical framework in which to describe it. This book deals with problems which we cannot expect to understand precisely and where many mathematical frameworks could apply. Our goal is to support argument about what the problem is like and to support the construction of solutions to it. This shifts our emphasis from choice of logic to its appropriate use and communication. Often the reason for modelling is automation. The forms of automation we describe are not well known so we want to work through them in detail using plausible, concrete examples. This is problematic because some of the technical details are distracting for people who have not seen that sort of thing before. Therefore, we have tried to reduce the density of formal definitions in the book by placing the more mundane material in supplementary world wide web (WWW) pages (http://www.dai.ed.ac.uk/groups/ssp/bookpages/blueprints.html) We have also concentrated on the operational aspects of the systems we describe rather than on the theoretical research which underpins them. Don't be offended if we have omitted your favourite engineering method or lifecycle model. We have tried to avoid specific methods where possible - partly because of our own limited experience but chiefly because the issues of concern to us are more general. Your compensation for this is that we introduce concrete examples rapidly and can discuss them within a uniform framework which does not force you into a particular methodological slot. To help you navigate we have placed ‘landmarks' as marginal notes. These are flagged differently by icons according to general topic: How to decide what best to do How to get it done How we describe what is done We hope that you will be motivated to build your own logical models. This skill is developed only through practice so we have included at the end of each chapter some short exercises to encourage you to strike out on your own. 0201398192P04062001