|| [News] || [Research]

AbadiLamport90 .Open AbadiLamport90 Martin Abadi & Leslie Lamport Composing Specifications Digital Sys Res Center(Oct 10 1990) CR9405-0309 F.3.1 .See [AbadiLamport93] =MATHEMATICAL SPECIFICATION LOGIC Has a ref to Cliff Jones's Oxford PhD Thesis in the early 80s! p9: "Composition is conjunction" cf Zave & Jackson. .Close AbadiLamport92 .Open AbadiLamport92 Martin Abadi & Leslie Lamport An Old-fashioned Recipe for Real Time Digital Sys Res Center TR#91(Oct 12 1992) .See [AbadiLamport94] =MATHEMATICAL TIMING LOGIC .Close AbadiLamport93 .Open AbadiLamport93 Martin Abadi & Leslie Lamport Composing Specifications ACM TOPLAS V15n1(Jan 1993)pp73-132 =MATHEMATICAL SPECIFICATION LOGIC Reviewed CR9405-0309 F.3.1 similar to AbadiLamport90 Based on Lamport91 .Close AbadiLamport94 .Open AbadiLamport94 Martin Abadi & Leslie Lamport An Old-fashioned recipe for Real Time ACM TOPLAS V16n5(Sep 1994)pp1543-1571 See .See [AbadiLamport92] =MATHEMATICAL TIMING LOGIC Review CR9507-0506 F.3.1: uses TLA as a base can reason separately about function and timing(by var now:real). Two problems: now can get stuck (Zeno-ness) or two requirements can conflict. ->> detect and correct spec to avoid. (not in A&L 1992?) .Close AbadiLamport95 .Open AbadiLamport95 Martin Abadi & Leslie Lamport Conjoining Specifications ACM Ttrans Prog Lang Sys V17n3(May 1995)pp507-535 CR9605-0369 CR9608-0610(...cumbersome notation....) F.3.1 =MATHEMATICAL SPECIFICATION LOGIC TLA conjunction implies parallel combination .Close Abiteboul00 .Open Abiteboul00 Serge Abiteboul & Peter Buneman & Dan Suciu Data on the Web: from relations to semistructured data and XML Morgan Kaufman SF CA 2000 ISBN 1-55860-622-X CR 0105-0161 QA76.9.D3 A258 =MONOGRAPH DATA NET/WWW LOGIC XML XSL-QL DTD ACeDB OEM Lore Strudel .Close AbramsonDahl89 .Open AbramsonDahl89 Harvey Abramson & Veronica Dahl Logic Grammars Springer Verlag 1989 =HOWTO GRAMMAR DDD PROLOG REALITY .Close Abrial89 .Open Abrial89 J Abrial A Formal Approach to Large Software Construction In Mathematics of Program construction J L A Van de Snepscheut(ed) Springer NY NY 1989 pp 1-20. See .See [LafontaneLedruSchobbens91] =ADVERT LOGIC TOOL Z VDM B B theorem prover LOGIC TOOL used by Z and VDM groups .Close AgarwalLago95 .Open AgarwalLago95 Rakesh Agarwal &Patricia Lago PATHOS - A Paradigmatic Approach To High-level Object-oriented Software Development ACM SIGSOFT Software Engineering Notes V20n2(Apr 1995)pp36-41 =ADVERT METHOD OBJECT-ORIENTED .Box confused technical activities: find classes, find methods and behavior, define classes and methods Technical control activities: logical design, detailed design ...Early consideration of reuse and quality in design .Close.Box .Close AielloEtAl07 .Open AielloEtAl07 Marco Aiello & Ian E Pratt-Hartman & Johan F van Bentham (Eds) Handbook of spatial Logics Springer Verlag NY Secaucus NJ 207 ISBN 1402055862 $CR 0811-1045 =UNREAD =REFERENCE FORMAL MODAL LOGIC SPACE .Close AikenMuntzRichards94 .Open AikenMuntzRichards94 Peter Aiken & Alice Muntz & Russ Richards DoD Legacy Systems: Reverse Engineering Data Requirements Comm ACM V37n5(May 1994)pp26-41 =EXPERIENCE REVERSE ENGINEERING DATA .Box 1.4 billion LOCs at 1.7K locations in thousands of different systems. 1986..87: Logical Data base Design 1992: First technologically independent logical data model LDM has 468 entities and 1994 data elements 1993: LDM has 362 entities and 1318 data elements .Close.Box .Close AlagarVenkatesan01 .Open AlagarVenkatesan01 Sridhar Alagar & Subbarayan Venkatesan Techniques to Tackle state explosion in a Global Predicate Detection IEEE Trans Software Engineering V27n8(Aug 2001)pp704-714 =THEORY LOGIC MODEL CHECKING .Close AlencarCowanLucena02 .Open AlencarCowanLucena02 Paulo S C Alencar & Donald D Cowan & Carlos J P Lucena A Logical Theory of Interfaces and Objects IEEE Trans Software Engineering V28n6(Jun 2002)pp548-575 =THEORY FORMAL LOGIC CATEGORY OBJECTS INTERFACES ADV ADO ADV ::= "Abstract Design Views", interfaces. ADO ::= "Abstract Design Objects". views_a::@(ADV, ADO). cf .See [AlencarCowanLucenaNova95] .Close AlexanderCoplien99 .Open AlexanderCoplien99 Christopher Alexander & James O Coplien(introduction) The Origins of Pattern Theory IEEE Software Magazine V16n5(Sep/Oct 1999)pp71-82 =SPEECH OOPSLA'96 PATTERN THEORY patterns were generative( ala Chomski ), included a moral component, must lead to morphological coherence - a life promoting structure, a good environment 15 geometric properties underlying original patterns -> profundity 80..90%agreement for "Do you feel more whole/alive in the presence of this or that object?". Correlates with certain features/structures & profound functionallity! centers:=field-like structures recursively underlying all wholeness& more or less living things. See .See [Alexander00] Can/will software designers help people generate a life enhancing world? .Close AmblerS97a .Open AmblerS97a Scott Ambler Normalizing Classes Software Development V5n4(Apr 1997)pp69-72 =DEMO DATA OBJECT-ORIENTED increasing cohesion and coupling by redesign but result is not in even 1NF in Codd terms. Adds a repeating group of enrollments to seminar. Better: Seminar<-<Enrollment>->Student and `new Enrollment(seminar student)` handles enrollments responsibillities for connecting seminars and students. Note: ends up with SSADM composite logical design! .Close AmbriolaNotkin88 .Open AmbriolaNotkin88 V ambriola & D Notkin Reasoning About Interactive Systems IEEE Trans Softw Eng SE-V14n2(Feb 1988)pp272-276 =THEORY LOGIC PROOF formal non-sequential .Close Ananthaswamy11 .Open Ananthaswamy11 Anil Ananthaswamy I, algorithm New Scientist V209n2797 (Jan 29 2011)pp28-31 =ADVERT =HISTORY AI LOGIC NEURAL NETS MARKOV BAYES PROBABILISTIC PROGRAMMING INFERENCE ENGINE LEARNING LANGUAGES BLOG Church BLOG::language="Bayesian logic". Demos of models with thousands of variables. General algorithms are inefficient. Applications: test ban treaty, PhysiScore(babies), QMR-DT Ref .See [Pearl88] .Close Anderson99 .Open Anderson99 Ross J Anderson The Formal Verification of a Payment System In .See [HincheyBowen99] pp43-52 =EXPERIENCE LOGIC BAN VERIFYING PROTOCOL BANKING PAYMENT SMARTCARD Used BAN_logic with new rule: If A believes that A and B share key K and A sees the K encrypts X then A will believe that B used K. Colored proof covering several white boards. System successful for several years with problems. Concludes the it better to have a simple logic with few rules and no tool than a complex (buggy?) logic with a tool. .Close Andrews93 .Open Andrews93 James H Andrews Logic Programming: Operational Semantics & Proof Theory Cambridge University Press NY NY 1993 ISBN 0-521-43219-7 CR9503-0142 =THEORY LANGUAGES .Close AndrewsP03 .Open AndrewsP03 Pater B Andrews Introduction to Mathematical Logic and Type Theory: to truth through proof Kluwer Acad Pub Norwell MA 2002 ISBN 1402007639 CR 0305-0427 =THEORY LOGIC TYPES LAMBDA PEANO .Close AntoniolGueheneuc06 .Open AntoniolGueheneuc06 Giuliano Antoniol & Yann-Gael Gueheneuc Feature Identification: an epidemiological metaphor IEEE Trans Software Engineering V32n9(Sep 2006)pp625-641 =DEMO MAINTENANCE TECHNICALREVERSE ENGINEERING TOOL CODE MODULE ANALYSIS A way to find out, by executing software the parts used to implement a feature. .Close Antoniou99 .Open Antoniou99 Grigoris Antoniou A Tutorial on Default Logics ACM ACM Computing Surveys V31n4(Dec 1999) pp337-359 CR0006-0401 =TUTORIAL FORMAL LOGIC DEFAULT INFERENCE EXCEPTIONS default :=`if Prereq : Justifications then Consequent`, `if Prereq then Consequent unless Justifications is known to be false` where no free variables in parts. default schema has free variables - stands for all substitutions. normal: `if P : J then J` closed world : `if true : not A then not A` Not just inferences but also extensions of sets known facts by applying defaults that don't lead to contradictions .Close AntoyHanus10 .Open AntoyHanus10 Sergio Antoy & Michael Hanus Functional Logic Programming Commun ACM V53n4(Apr 2010)pp74- 95 .See http://doi.acm.org/10.1145/1721654.1721675 =ADVERT CURRY LANGUAGE FUNCTIONAL LOGIC PROGRAMMING Combines ideas from functional programming (LISP, ML, Haskell) and Logic Programming (Prolog). Given a definition of a function Curry can sometimes invert it, finding argument values to fit given results. .Close Aptetal80 .Open Aptetal80 Krzysztof R Apt & Francez & De Roever A Proof System for Communicating Sequential Processes ACM TOPLAS V2n3(Jul 1980)pp359-385 =THEORY LOGIC CSP formal .Close Asaravala03 .Open Asaravala03 Amit Asaravala All by themselves Software Development Magazine V11n3(Mar 2003)pp38-41 =HISTORY AGENTS AI Clippy metadata semantic web XML RDF ontology DAML+OIL LOGIC Agents (minimally) observe an environment and react to changes by interacting with the environment -- and other agents. Agents either need a shared ontology or a way to share ontologies and metadata. RDF::XML_DTD="Resource Description Framework", indicates relationships between subjects, predicates and objects. .Close Astrachan91 .Open Astrachan91 Owen Astrachan Pictures as Invariants SIGCSE Bulletin V23n1(Mar 1991)pp112-118 =DEMO LOGIC TECHNICAL GRAPHIC .Close AtleeBuckley96 .Open AtleeBuckley96 Joanne M Atlee & Michael A Buckley A logic-Model Semantics for SCR Software Requirements Proc 1996 Int Symposium on Software Testing & Analysis(ISSTA) & ACM SIGSOFT SENotes V21n3(May 1996)pp280-292 =IDEA LOGIC SCR REQUIREMENTS TABULAR SCR::="Software Cost Reduction" SCR Statecharts RSML all share conditioned-event-driven reactive systems. demos analytical requirements temporal logic model and tool SMV::="Symbolic Model Verifier". CTL::=Computational Tree Logic See CORE .See [WilliamsL94] .See [HeimdahlLeveson96] .Close Bach95 .Open Bach95 James Bach Enough about process: What we need are heroes IEEE Software Magazine V12n2(Mar 1995)pp96-98+replies IEEE Software Magazine V12n3(May 1995)p5-7 .See [Bach9?] .Box "Heroism means going beyond the borders of the known world and returning with new knowledge or wealth[...]sustainable, healthy sort of heroism requires judgement to know how much commitmment and risk is right for the situation. The movement towards process in our industry is an understandable reaction against pathological heroism: heroism for its own sake, in which overcommitment and uncontrolled risk-taking is the norm." p97: "The 'cowboy' or 'big magic' model. In this view, gifted people create software through apparent magical means, with no particular guidance or support" Can integrate process and heroism by taking a people centred view and seeing software production as a dynamic, complex, etc. system for solving problems. Reply: John Henry or Pecos Bill, trial by cold pizza,... .Close.Box .Close BaclawskiIndurkhya94 .Open BaclawskiIndurkhya94 Kenneth Baclawski & Bipin Indurkhya The Notion of Inheritance in object-oriented programming(Letter) Commun ACM V37n9(Sep 1994)pp118-119 .See [Grosberg93] .See [ArnoldK94] (C++ advice) .Box refers to debate over meaning of inheritance: Abrahams's 91 letter "Subject: Objectivism" Lalonde & Pugh JOOP 91 "subclassing <> subtyping <> is-a" Tesler's 91 CACM letter Wegner 80 pages in 90 OOPS messenger Winkler 92 letter refers to POV vs COV in Winkler's letter Quotes Wegner 90 POV = Physical & COV = Conceptual Piaget: Child constructs idea of object permanence from its own actions on the objects. Class of objects without actions<>class of objects with some actions. Failure to find epistomological foundations of the IS-A link - six different generic-generic and four kinds of generic-individual relation "The point here is that the concepts in the real world, which programs attempt to model, do not come in neatly packaged hierarchies." (cf GoldsteinAlger92) "There are no standard conceptual hierachies. Given a domain and a specific PURPOSE, certain concept hierarchies would be clearly preferable than others, but such policy decisions are best left to the USER of the programming language[...] What a PL provides is a set of mechanisms [...] restrict what can be implemented[but] they do not themselves validate some view of inheritance or other[...]" these are also just implemented concepts and do not not have a universal objective meaning....upto the designers to choose suitable mechanisms. .Close.Box .Close BaierHaverkortHermansKatoen03 .Open BaierHaverkortHermansKatoen03 Christel Baier & Boudewijn Haverkort & Holger Hermans & Joost-Pieter Katoen Model-checking algorithms for continuous-time Markov Chains IEEE Trans Software Engineering V29n6(Jun 2003)pp524-541 =THEORY MATHEMATICS MODEL CHECKING CTMC CSL RELIABILITY CTL CSL:="Continuous Stochastic Logic". Steady state + path probabilities in time intervals. Modes P[event] <=> p. Nested. Generalizes CTL. CTMC::="continuous time Markov chains". P(i -> j fires after t) = c*exp( -rate*t) iff it is first. .Close BaierEtAl07 .Open BaierEtAl07 Christel Baier & Lucia Cloth & Boudewijn R Haverkort & Mathias Kuntz & Markus Siegle Model Checking Markov Chains with Actions and State Labels IEEE Trans Software Engineering V33n4(Apr 2007)pp209-224 =THEORY MODEL CHECKING REAL TIME MARKOV CHAINS PROBABILITY LOGIC asCSL Logic + model design for verifying requirements that a given pattern of actions and states (and time limits) has a given range of probabilities. Example requirement: the probabillity of entering a `full` state via a number of `arrive` actions within 5 time units must be greater than or equal to 99%. Defines products of chains. Cellular phone hand over model. experiment with tool. .Close BaierKatoen08 .Open BaierKatoen08 Christel Baier & Joost Katoen Principles of Model Checking The MIT Press Cambridge MA (2008) ISBN 026202649X $CR 0912-1115 =TEXT =THEORY MODEL CHECKING MODAL LOGICS FSM LTL CTL CTL* TCTL BISIMULAION OBDT MARKOV PCTL PCTL* Excellent and thorough text book suitable for graduate Computer scientists or some final year undergraduates A large in depth reference to the theory of the most successful formal methods - so far. Does not use the normal syntax for modes but uses \forall and \exists. So doesn't fit some tools. Does not use standard terminology. Does include newer topics and types of models. .Close BaierHaverkortHermansKatoen10 .Open BaierHaverkortHermansKatoen10 Christel Baier & Boudewign R Haverkort & Holger Hermans & Joost-Pieter Katoen Performance Evaluation and Model Checking Join Forces Commun ACM V53n9(Sep 2010)pp76-85 .See http://doi.acm.org/10.1145/1810891.1810912 =HISTORY MODEL CHECKING PERFORMANCE MODAL PROBABILLITY LOGIC CTL LTL PCTL DTMC ADVERT TOOLS PRISM EXAMPLES Excellent diagram of history starting with Markov Chains in 1900 and ending with advanced algorithms and applications. Figure 3: IPv4 zeroconf protocol Example -- able to show that Firewire root contention protocol is faster when biased "coin tossing" is used. .Close Ballanceetal90 .Open Ballanceetal90 Robert A Ballance & Susan L Graham & Michael L Van De Vanter The Pan Language-Based Editing System for Integrated Development Environments SIGSOFT'90 pp77-93 p85 Logic programming .Close BarbierEtal03 .Open BarbierEtal03 Franck Barbier & Brian Henderson-Sellers & Annig Le Parc-Lacarelle & Jean-Michele Bruel Formalization of the Whole-Part Relationship in the Unified Modeling Language IEEE Trans Software Engineering V29n5(May 2003)pp459-470 Reviewed $CR 0409-1078 and 0409-1079 =PROPOSAL Object-Oriented MODEL STANDARD aggregation composition whole-part bibliography UML OCL MetaModel OML OPEN Diamonds careful philosophical analysis of semantics of whole-part. some confused "common logic" and much OCL. Defines a new dotted diamond whole-part Relationship with specialization of aggregation and composition. Introduces new stereotypes to indicate OCL constraints on the UML MetaModel. Will it make it into UML4.0? Correspondence .Box IEEE Trans Software Engineering V29n11(Nov 2003)pp1054-1056 "On formalization of the whole-part relationship in the unified modeling Language" by Hee Beng Kuan Tan & Lun Hao & Yong Hang corrects discrepancies, "Controversies about the Black and White Diamonds" by Frank Barbier & Brian Henderson-Sellers" responds by changing name of "antisymmetry", accepting new formula for "transitivity", and agreeing to minor correction in a proof. Regrets the absence of "scientific" review of UML specifications. .Close.Box .Close Barjis08 .Open Barjis08 Joseph Barjis The importance of business process modeling in software systems design Science of Computer Programming V71n1(Mar 2008)pp73-87 .See http://www.sciencedirect.com/science $CR 0906-0558 =ADVERT METHOD THEORY MODEL DEMO LANGUAGE-ACTION PETRI GRAPHIC ANALYSIS REQUIREMENTS SCENARIOS Keywords: Requirements specifications; Model checking; Business process modeling; Business process simulation; DEMO::="Design & Engineering Methodology for Organizations", .See http://www.demo.nl/ Special colored Petri nets show logic. Can be simulated to show clients what is possible. Analyze business processes in terms of the language-action cycle as expressed as $Transactions between parts. Transaction::=Order; Execution; Result. Order is a transition from initiator to executor. It sets up a contract for the executor to carry out. Result is a transition from executor to initiator. It completes the contract. Execution is executed by the executor and can initiate further transactions with others. .Close Barnhart99 .Open Barnhart99 Andy Barnhart Wrapping COBOL Business Logic in Java Software Development Mag V7n10(Oct 1999)pp41-45. =EXPERIENCE TECHNICAL COBOL JAVA GUI LEGACY MARS UK RLSCOM Telco marketting cellular air time .Close Barrett87 .Open Barrett87 Geof Barrett Formal Methods Applied to a Floating Point Number System Technical Monograph 58 PRG Oxford 1987 =EXPERIENCE PROOF Floating-point operations STANDARD .Box used Hoare/Floyd-style proofs to prove that Inmos' software floating-point package satisfied its specification, a Z-ified version of the IEEE-754 standard. This software fp package was the starting point for the formally-derived microcode for the FPU in the Inmos T800 transputer. This was certainly a real-world application; moreover, the formal approach overtook the informal approach, and in the process they found an inconsistency and an ambiguity in the IEEE standard, and a bug in a competitor's chip. Inmos and the PRG (Oxford) were awarded a Queen's Award for Technological Achievement for the T800 project. Includes Floating point IEEE TSE paper -- where is it? .Close.Box .Close BaudryEtal05 .Open BaudryEtal05 Benoit Baudry & Franck Fleurey & Jean-Marfc Jezequel & Yves Le Traon Automatic Test Case Optimization: A Bacteriologic Algorithm IEEE Software Magazine V22n2(Mar/Apr 2005)pp76-81 =IDEA C# PARSER BUILDER VISITOR TESTING MUTATION EVOLUTION FITNESS Nice use of patterns in the sample Component Under Test (CUT) a C# parser. Need 30 generations to produce a set of tests that could `kill` all 500 mutants. .Close Beck01 .Open Beck01 Kent Beck Aim, Fire IEEE Software Magazine V18n5(Sep/Oct 2001)pp87-89 =DEMO TESTING first is ANALYSIS DESIGN SPECIFICATION "Never write a line of functional code without a broken test case". Ward Cunningham: "Test-first coding is not a testing technique". Writing tests helps you understand the problem: analysis. Writing tests described the logic of the design. Hard to write GUI tests. Claim that creatively lazy test-first coding tends to be more cohesive and less coupled -- because the interfaces tend to be minimized to saving typing: "intense feedback substitutes for the ability to guess right" Test cases expose misunderstandings in pair programming. Test cases document the all important answer to "What was this idiot thinking when he wrote this?". .Close Beeson81 .Open Beeson81 Michael J Beeson Formalizing Constructive Mathematics: Why and How? Constructive Mathematics Spring Verlag Lecture Notes in Mathemetics V873 pp146-190 1981 =THEORY FORMAL LOGIC LPT::="Logic of Partial Terms" Compare .See [Schock68] .See [Parnas93] .See [JonesCB95] and .See [PVS] LPF:=Logic of Partial Functions .Close BelliniMattoliniNesi00 .Open BelliniMattoliniNesi00 P Bellini & R Mattolini & P Nesi Temporal Logics for Real-time system specification ACM Computing Surveys V32n1(Mar 2000) pp12-42 =SURVEY LOGIC TIMING RTL RTIL RTTL WWW link to ACM Digital Library: .See http://www.acm.org/pubs/citations/journals/surveys/2000-32-1/p12-bellini From Abstract: The specification of reactive and real-time systems must be supported by formal, mathematically-founded methods in order to be satisfactory and reliable. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulas, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few years can be used for specifying reactive systems, although not all are suitable for specifying real-time systems. In this paper we present a series of criteria for assessing the capabilities of temporal logics for the specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specifications is identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples. .Close Ben-Ari10 .Open Ben-Ari10 Mordechai (Moti) Ben-Ari A Primer on Model checking ACM Inroads V1n1(Mar 2010)pp40-47 =ADVERT =EXAMPLES MODEL CHECKING EDUCATION Spin VN Erigone NDFA NON_SEQUENTIAL VERIFICATION MODAL LOGIC Promela IDE The formula `if not p then if p then q` can be proved true by axiomatic methods but it is simpler and easier to check that it is true by trying out all 4 cases in a truth table. Similarly, proving that a parallele non-deterministic program has a property is usually time consuming but there exist tools that will find counter examples in a reasonable time. Spin works in industry but can be wrapped in an IDE that works well with students. .Close BergmanMoorNelson90 .Open BergmanMoorNelson90 Merrie Bergman & James Moor & Jack Nelson The Logic Book (2nd edn) McGrawHill (1990) ISBN 0-07-909524-0 LC# BC135.B435 =TEXT FORMAL LOGIC NATURAL DEDUCTION TREES SEMANTIC TABLEAUX .Close BerryKamsties05 .Open BerryKamsties05 Daniel M Berry & Erik Kamsties The syntactically dangerous ALL and Plural in Specifications IEEE Software Magazine V22n1(Jan /Feb 2005)pp55-57 =IDEA AMBIGUITY LOGIC LANGUAGE SPECIFICATION CS565 Words to suspect: "only", "all", "also", "each". Use "each" when describing a property of the individual members of a set. Use "all" for shared properties across a set. Can use simple logic to clarify an ambiguity. All the lights in the room have a single on-off switch. .Net Each light has its own switch. For all y:lights_in_room, one x: switch (x is on_off_switch_for y). All the lights share a common switch. For one x: switch, all y:lights_in_room (x is on_off_switch_for y). .Close.Net Similarly for plurals: "Students enroll in six courses" vs "Students enroll in hundreds of courses". .Close BeyerNoackLewerentz05 .Open BeyerNoackLewerentz05 Dirk Beyer & Andreas Noack & Claus Lewerentz Efficient Relational Calculation for Software Analysis IEEE Trans Software Engineering V31n2(Feb 2005)pp137-149 =TOOL RELATIONAL LOGIC RML BDD TECHNICAL PATTERN JAVA CrocoPat Faster recognition of patterns in class structures tested faster on real code: JDK AWT, Eclipse,... Than Prolog and MySQL. .Close BiZhao04 .Open BiZhao04 Henry H Bi & J Zhao Applying propositional logic to workflow verification Information Technology and ManagementV5n3-4(Jul wppr)pp293-318 $CR 0605-0526 =UNREAD =THEORY WORKFLOW VERIFICATION LOGIC .Hole .Close Blikle77 .Open Blikle77 Andrzej Blikle Co-Routines and Networks of Parallel Processes Proc IFIP 77 (North Holland Pub Co 1977) pp285-290. Also IRIA Raport de Recherche No 202 Nov 76 =THEORY LOGIC SEMANTICS REGULAR-EXPRESSIONS .Close Bliss42 .Open Bliss42 Charles K Bliss Semantography ( Blissymbolics) 2nd Edn Semantography ( Blissymbolics), Sydney Australia 1942 .See http://www.semantography.com/ =ADVERT GRAPHIC SYMBOLIC LANGUAGE GENERAL SEMANTICS RATIONALITY LOGIC Explains BlissSymbolics. Argues that Semantography helps spot crooked thinking and false arguments. Bliss Symbols include all internationally agreeed symbols: Math, Chem, Music,... Dictionary of symbols .See http://www.semantography.com/4/ .Close BloomEsik93 .Open BloomEsik93 Stephen L Bloom & Zoltan Esik Iteration Theories: Equational Logic of Iterative Processes EATCS monographs on Theoretical Computer Science Springer Verlag NY NY 1993 ISBN 0-387-56378-4 CR9505-0287 630 pages $109.00 Hardcover =MATHEMATICAL LOGIC ALGEBRA SEMANTICS .Box Blurb: detailed investigation of the fixpoint/iteration operation. Universal Algebra. Correctness logic is a special case of the equational logic of Iteration theories. Ten year program... see Bloom83 CR9505-0287: categegory theory, slow and casual, nonstandard power functor, doesn't discuss dynamic algebras, algebras with star, action algebras, or process algebras. .Close.Box .Close BojicVelasevic00 .Open BojicVelasevic00 Dragan Bojic & Dusan Velasevic Reverse Engineering of Use Case Realizations in U ML ACM SIGSOFT Software Engineering notes V25n4(Jul 2000)pp56-61 =IDEA VisualC++ TEST profiling LOGIC DA-C use concept analysis to convert profiles of test executions into lattices of use-cases .Close BoralvStalmarck99 .Open BoralvStalmarck99 Arne Boralv & Gunnar Stalmarck Formal Verification in Railways In .See [HincheyBowen99] pp329-350 =EXPERIENCE RISKS SPECIFICATION STD/FSM LOGIC TPA vs DESIGN V&V TOOL Prover Delphi for ADtranz CVT Swedish Sternol Prover is a Company specializing in the industrialization of formal methods. Stalmarck has patented the proof algorithm! Can we make a formal tool that is as transparent to use as a word processor? Some parts need a formal methods expert, but some parts can be made more useful to railway interlocking engineers. Need to trade-off expressive power of logic with the performance of the tool. Claims that ONLY domain/application knowledge is needed to use the tools. .Close BorgerSchulte00 .Open BorgerSchulte00 Egon Bo"rger & Wolfram Schulte A Practical Method for Specification and Analysis of Exception Handling -- A Java/JVM Case Study IEEE Trans Software Engineering V26n9(Sep 2000)pp872-887 =CASESTUDY LOGIC SPECIFICATION SEMANTICS JAVA COMPILER JVM PROOF .Close Borgidaetal95 .Open Borgidaetal95 Alex Borgida & John Mylopoulos & Raymond Reiter The frame problem in procedure specifications IEEE Trans on Software Eng VSE-SE-21n10(Oct 1995)pp785-798 =CRITIQUE LOGIC Set Theory SPECIFICATION METHODS circumscription .See [BorgidaMylopoulosReiter93] .Find JacksonD9 .See [McCarthy87] .See [Delgrande98] .Close BorgidaJarke92 .Open BorgidaJarke92 Alex Borgida & Mathias Jarke Knowledge and Representation in Software Engineering(Editorial on special issue) IEEE Trans SE-18n6(Jun 1992)pp449-450 CR9307-0467 domain logic ... relation to formal methods ... power vs performance ... empirical results .Close Botting78a .Open Botting78a Richard J Botting Loglan -- a more flexible language =ADVERT Loglan Mathematics Logic ITL UNIVERSAL LANGUAGES Computer Weekly (UK) n598 (Feb 16 1978)letters Response to .See [Kelly78] Argues that Loglan fits Kelly's criteria better. .Close Botting86a .Open Botting86a RJ Botting Into the Fourth Dimension: An Introduction to Dynamic Analysis & Design SE Notes v11 n2 pp36-48 Apr 1986 ACM SIG Software Engineering =THEORY DAD graphic logic Reality .Close Botting87b .Open Botting87b RJ Botting Regular Expressions Relations & Software: Part I - Practice & Part II - Theory Western Educational Computing Conference Nov 1987 Western Periodicals Co. N Hollywood CA. =THEORY DDD JSP theory languages logic formal .Close Boute00 .Open Boute00 Raymond T Boute Supertotal function definition in Mathematics and Software Engineering IEEE Trans Software Engineering V26n7(Jul 2000)pp662-672 =IDEA FORMAL LOGIC FUNCTIONAL MATHEMATICS calculational Refers to FunMath .See [PVS] .See [Parnas93] Compare: .See [LPT] Question: How to calculated easily with partial functions? Idea: Functions defined by a domain and an expression can be treated as total by extension to an arbitrary value in calculating with suitably guarded formulae .Close BowdigeGriswold98 .Open BowdigeGriswold98 Robert W Bowidge & William G Griswold Supporting the Restructuring of Data Abstractionns through Manipulation of a Program Visulaization ACM TOSEM V7n2(Apr 1998)pp109-157 =TOOL TECHNICAL GRAPHIC ADT REENGINEER .Close Bowen00 Jonathon Bowen The Ethics of Safety-Critical systems Commun ACM V43n4 (Apr 2000)91-97 =ESSAY RISKS METHODS Aristotle LOGIC 7 sins: epideictic, hyperole, pistic, oligarchy, ephemeral, epexegesis , maiandos principles modes of thought: scientific, technical, prudence, inntelligence/intuition, wisdom p93: "most theorems are correct, but most hand proofs are wrong" .Close Bowen01 .Open Bowen01 Jonathon P Bowen Experience Teaching Z with TOOL and Web Support ACM SIGSOFT Software Engineering Notes V26n2(Mar 2001)pp69-75 =REPORT UK TEACHING MATHEMATICAL LOGICAL SPECIFICATION REFINEMENT TOOLS ZTC ZANS Diagnostic quizzes leading to makeup tutorials help handle wide ranges of math skills. .Close BowenHinchey94 .Open BowenHinchey94 Jonathan P Bowen & Michael G Hinchey Formal Methods andSafety Critical Standards IEEE Computer Magazine V27n8(Aug 1994)pp68-71 .Box Quotes IEEE standard definitions Most standards are reccommending formal methods rather than mandating them or using them. Table 1, p70: shows that only 1 out of 5 US standards has FMs, but all 7 non-US standards have FMS FMs mentioned in standards: CCS(2), CSP(2), HOL(2), LOTOS(2), OBJ(2), Temporal Logic(2), VDM(3), Z(4) .Close.Box .Close BrewkaEiterTruszczynski11 .Open BrewkaEiterTruszczynski11 Gerard Brewka & Thomas Eiter & Miroslav Truszczynski Answer set programming at a glance Commun ACM V54n12(Dec 2011)93-103 .See http://doi.acm.org/10.1145/2043174.2043195 =ADVERT DEFEASIBLE LOGIC DECLARATIVE PROGRAMMING ASP GROUNDERS SATISFY SAT SEMANTICS TOOLS APPLICATIONS ABBREVIATIONS a <- b1,...,bm, not c1, ..., not cm. where a,b,c... are "predicates'. Answer set is a set of predicates that can be derived if we assume certain predicates are true/false and is not contradicted by the derivable predicates. Able to express if-then-else and constraints easily and a number of other formulas that appear in practice. Can handle predicates that contain variables by reducing them. .Close Britcher96 .Open Britcher96 Bob Britcher A Few (proposed) fundamental laws of programming IEEE Computer Magazine V29N3(Mar 1996)p136(Open channel) .Box The Law of Rapid Specialization In programming major changes in the product can occur in an instant vs time to change plant or physical products The Law of Fallibility The most careful reasoning about a simple sentence can lead to a wrong conclusion about the real world Programmers have to reduce big "word-problems" to logic. The Law of Intellectual Gravity Programs can be as massive(in there own way) as physical objcts. The Law of Permannence Programs do not become extinct. They are not discarded, they are piled up, combined, absorbed, breeding and spreading. .Close.Box .Close BrockHunt99 .Open BrockHunt99 Bishop C Brock & Warren A Hunt Jr Formal Analysis of the Motorola CAP DSP In .See [HincheyBowen99] pp- =EXPERIENCE HARDWARE DESIGN V&V VERIFICATION FORMAL LOGIC TOOL ACL2 .Close BrownP91 .Open BrownP91 Patrick Brown Integrated hypertext and program understanding tools IBM Syst J V30n3(1991)pp363-392 =TOOL TECHNICAL CR 9211-0872(N Zvegintov) .Box CR92011-0875 is by N Zvegintov and refers to the lack of tools to record and maintain links between the domain and the implementation. Multiple{languages, platforms(IBM), uses, data/tools} ISEA Integrated SoftwareEngineering Applications tools platform OS/2 + VM + MVS, Distributed client &/| server CodeNavigator helps programmers {undertand software, analying change requests, Diagnosis} {what, where, how}-used, flows{logic, calling,...}, annotations, source code brousing p369 "Program analysis can create databases that may grow to many times the size of the original source library" 500KLOC -> too big for wkstn DB Staged analysis, raw vs derived data flexible USER interfaces TRAILS::= prototype hypertext tool linking program data - HIPO | lexical afinity |Data model attributes p389: "Lost in Hyperspace" - "loosing track of what they are looking at or how they got there" .Close.Box .Close Broy11 .Open Broy11 Manfred Broy Can Practitioners neglect theory and theoreticians Neglect practice? IEEE Computer V44n10(Oct 2011)pp19-24 =ESSAY GAP THEORY ENGINEERING Theory should help establish terminology, techniques, and measurements. Practicioners have provided good ideas but where is the scientific tests of these theories? Craft, Science, or Engineering? Theory should help organize knowledge -- both domain and technical knowledge A method/methodology may not have an explicit theory and probably: does not scle, is too difficult, not well designed, and not cost-effective. Theory should be part of a software enginmeers education: operating systems, data bases, protocols, formal languages, semantics,... .Key informatics, sociology,... Theory in research: based on empirical data, isolated, vs ad hoc methods. We do not need beautiful theories -- we need to solve particular problems. Other forms of engineering a based on separate sciences... software engineering depends on logics and theories of information and computation. .Close Buchi02 .Open Buchi02 J R Buchi On a Decision Method in Restricted second-order arithmetics Proc Int'l Conf. Logic, Methods and philosophy of science (1962) pp1-12 =THEORY AUTOMATA omega-automata Buchi-automata Given a standard finite state automata with accepting states its language is defines a set of infinite strings that are acceptable: they can return an infinite number of times to at least on of the accepting states. .Close Burge91 .Open Burge91 T Burge Truth and Singular Terms in Philosophical Applications of Free Logic Oxford Univ Press 1991 pp 189-204 =THEORY FORMAL LOGIC See .See [LPT] and .See [LPV] .Close BurrowsAbadiNeedham89 .Open BurrowsAbadiNeedham89 M Burrows & M Abadi & R M Needham A Logic of Authentication Proc Royal Society of London A V426(1989)pp233-271 =THEORY FORMAL LOGIC BAN_logic::Logic, logic of authentication -- who can believe what about whom? .See http://csci.csusb.edu/dick/samples/BAN.html See also .See [BurrowsAbadiNeedham90] .Close BurrowsAbadiNeedham90 .Open BurrowsAbadiNeedham90 Michael Burrows & Martin Abadi & Roger M Needham A Logic of Authentication ACM Transactions on Computer Systems V8n1(Feb 1990)pp18-36 .See http://doi.acm.org/10.1145/77648.77649 =THEORY =DEMO LOGIC PROTOCOL PROOF V&V BAN KERBEROS CRYPTO See also .See [BurrowsAbadiNeedham89] Defines the .See [BAN_logic] of beliefs and messages. .Close CalcagnoOHearnBornat03 .Open CalcagnoOHearnBornat03 C Calcagno & P OHearn & R Bornat Program logic and equivalence in the presence of garbage collection Theoretical Computer Science V298n3(??? 2003)pp557-581 =THEORY FORMAL LOGIC HOARE Garbage Collection (D.4.2) VERIFICATION What do we mean when we say that a particular object "exists" on the heap? To preserve Hoare's assignment axiom in the presence of garbage collection, the existence of garbage becomes "virtual". The wise program prover should use a language with proved automatic garbage collection, and avoid assertions that refer to garbage! Includes a formal model of garbage collection. .Close CalinescoGhezziKwiatowskaMirandola12 .Open CalinescoGhezziKwiatowskaMirandola12 Radu Calinescu & Carlo Ghezzi & Marta Kwiatowska & Raffaela Mirandola Self-adaptive Software needs Quantitative Verification at runtime Commun ACM V55n9(Sep 2012)pp69-77 .See http://doi.acm.org/10.1145/2330667.2330686 =THEORY ADAPTIVE PERFORMANCE MONITOR ADJUST DTMC PCTL SERVICE Need to verify: `If Specification and Domain then Requirement`. Non-standard activity diagrams look good... Markovian model of the specification, Probalistic Computer Treel Logic requirements. Domain data comes from monitoring service performance. System can switch components if performance is bad. .Close Camilleri90 .Open Camilleri90 Albert John Camilleri Mechanizing CSP Trace Theory in Higher Order Logic IEEE Trans Software Engineering SE-V16n9(Sep 1990) .Close Campbell-Kelly10b .Open Campbell-Kelly10b Martin Campbell-Kelly Historical Reflections: Victorian Data Processing Commun ACM V53n10(Oct 2010)pp19-21 .See http://doi.acm.org/10.1145/1831407.1831417 =HISTORY DATA PROCESSING LOGICAL vs PHYSICAL BABBAGE CLEARING CHECKS USA CHEQUES UK Shows an efficient solution to a problem in the form of a multi-agent procedure. Traces the evolution of Bank Clearing Houses in the UK (as documented by Babbage) and then in the USA. Argues that similar algorithms are still used in modern information technology. .Close Canforaetal92 .Open Canforaetal92 Gerardo Canfora & Anielo Cimitile & Ugo de Carlini A Logic-Based Approach to Reverse Engineering Tools Production IEEE Trans on Software Eng VSE-18n12(Dec 1992)pp1053-1064 .Box Prolog model of a Pascal-like program gives queriable data base/knowledge base. Implemented on silicon/UNSW Prolog. .Close.Box .Close CaplanHarandi95 .Open CaplanHarandi95 Joshua E Caplan & Mehdi T Harandi(*@cs.uiuc.edu) A Logical Framework for Software Proof Reuse .See [SamadzadehZand95] pp106-113 =THEORY DEMO PROOF REUSE Hoare triples do not have referential transparency! .Box Created a new quantifier to bind (and hide) program identifiers into a context and protect them from sustitution. deca;arations also bind identifiers (and so hide them). Assignment axiom: for_vars x( {P(t=>x[m])} x[m]:= t {P} ). Declaration axiom: for_vars x({ P and x[m]=e} C{Q}) ---------------------------------------------------where x=y,x[m],z. for_vars y,z( {P} new x[m]:=e ; C {Q} ) .Close.Box .Close Carroll94 .Open Carroll94 John M Carroll<carroll@cs.vt.edu> Making Use a Design Representation Commun ACM V37n12(Dec 1994)pp29-35 =EXPERIENCE USER scenario use-case .Box Scenarios have always been an informal but useful part of documentation. Make them the prime representation of the system instead -- reason with them.... Also include analysis of psychological effects of technical decision: IN <situation> <a feature> CAUSES < + effect> BUT MAY ALSO CAUSE < - effect> .Close.Box .Close CarrollL77 .Open CarrollL77 Lewis Carroll (ed. William W Bartley III) Symbolic Logic Pts I & II Harvester Press 1977 Hassocks Sussex England =MONOGRAPH LOGIC syllogisms SORITES EXAMPLES Pt II uses something like resolution and semantic tableaux! .Close CerroGasquet02 .Open CerroGasquet02 Luis Farnias Del Cerro & Olivier Gasquet A General Framework for Pattern-Driven Modal Tableaux L J of the IGPL V10n1(2002)pp51-83 =THEORY PROVING MODAL LOGIC SEMANTIC TABLEAUX RELATIONS Proves completeness and soundness for a set of rules for proving formula in many different modal logics by combining Kripke semantics, semantic Tableaux, and relational calculus. p58 rule <>: If <>A,S @ p then add node q: <>A,S@p ---A@q. rule K: if []A,S@p----S1@q then []A,S@p----A,S1@q. Lotrec::tool=http://www.itit.fr/ACTIVITIES/LILaC/Lotrec/, written in Java .Close Cervanto00 .Open Cervanto00 Iliano Cervanto Logical Framework: Why not just classical logic? CSLI Lecture notes V91, Stanford U(2000)pp87-104 in "Formalizing the dynamics of information" ed. Martina Faller & Stefan C Kaufmann & Marc Pauly ISBN 1-57586-239-5 Q360 =ESSAY LOGIC LAMBDA cf Z SCHEMA (dick) |- Parallels my thinking in creating MATHS. .Close Chalin10 .Open Chalin10 Patrice Chalin Engineering a sound assertion semantics for the verifying compiler IEEE Trans Software Engineering V36n2(Mar/Apr 2010)pp275-287 =TYPE USER V&V SQA FORMAL METHOD TOOL VC VERIFICATION COMPILER A verifying compiler should spot when assertions will go wrong. The logic of the verifying compiler should allow for expressions being undefined. Must handle arithmetic errors like 1/0 correctly. Even in assertions! Stresses the need to talk to the users of the compiler before deciding its semantics! Introduces a definedness predicate. Formal Methods shouldn't have imposed an elegant but unsound logic on software. .Close Champeaux02 .Open Champeaux02 Dennis de Champeaux Software Engineering Considered Harmful Commun ACM V45n11(Nov 2002)pp102-104 =ESSAY ENGINEERING SCIENCE LOGIC PRACTICE C++UML VALIDATION Quotes Denning on the state of current software systems and being hired to fix messes that should not have occurred. Need for extensions to Hoare Logic to pointers and parallel processes. Seems to ignore work by Hoare, Lamport and others. .Close ChanEtal01 .Open ChanEtal01 William Chan & Richard J Anderson & Paul Beame & David H Jones & David Notkin & William E Warner Optimizing symbolic Model checking for Statecharts IEEE Trans Software Engineering V27n2(Feb 2001)pp170-190, also in ICSE'99 =EXPERIMENTS FORMAL VERIFICATION REQUIREMENTS STATECHARTS GRAPHIC LOGIC OPTIMIZATION RSML TCAS II BDD Electrical power distribution system order of magnitude improvements. .Close ChariSeshadri04 .Open ChariSeshadri04 Kaushal Chari & Saravanan Seshadri Demystifying Integration Commun ACM V47n7(Jul 2004)pp59-63 =TAXONOMY STANDARDS BUSINESS (industry domain (independent | dependent ))><((data | business | presentation ) logic)><(( transport | data format | process ) level) .Close ChechikDevereuxEasterbrookGurfinkel04 .Open ChechikDevereuxEasterbrookGurfinkel04 Marsha Chechik & Benet Devereux & Steve Easterbrook & Arie Gurfinkel Multi-Valued Symbolic Model-Checking ACM TOSEM Trans Software Eng & Methodology V12n4(Oct 2003)pp371-408 =IDEA TOOL MODEL CHECKING CTL FSM Kripke Multi-valued LOGIC Quasi-Boolean Lattice \Chi\_CTL \Chi\_Check \Chi\_Kripke Extends classical {False, True} reasoning to {False, Maybe, True} values. Good for incomplete models found during analysis. Able to have multi-valued variables in: state of FSM, Transitions between states, satisfaction. meaning(EX(p)) := backward_image(RR)(meaning(p)). backward_image(RR)(TT) := map[s:S](multivalued_union[t:T](TT(t) multivalued_intersection RR(s,t) )). Implementation described in 2002 CSRG Tech Report 446, University of Toronto .Close Cheek95 .Open Cheek95 Martin Cheek Using Feedback to Improve Software Development IEEE Software Magazine V12n3(May 1995)pp89-90 =REPORT FEAST EVOLUTION PEOPLE SYSTEMS .Box Reports on research by Manny Lehman<mml@doc.ic.ac.uk> - complex social interactions explains why 20 years of technological innovations do not correspond with a significan improvement in the development process. The "Feast" Feedback Evolution And Software Technology. .Close.Box .Close ChesnevarMaguitmanLoui00 .Open ChesnevarMaguitmanLoui00 Carlos Ivan Chesnevar & Ana Gabriela Maguitman & Ronald Prescott Loui Logical models of argument ACM Computing Surveys V32n4(Dec 2000)pp337-383 =HISTORY 1950-99 FORMAL DIALECTIC DEFEASIBLE CONSISTENCY REASON ARGUMENT PLAUSIBLE AGENTS AI LAW NONMONOTONIC Formal logic is reasoning that can not be defeated. Normal reasoning is not like this. Detailed, difficult and hard to read. No ref to work on inconsistent requirements. Small comment on OO inheritance. .Close Christy09 .Open Christy09 Peter Christy Commentary: A Trip without a Roadmap ACM Queue V7n1(Mar 2009) .See http://queue.acm.org/detail.cfm?id=1515746 =CASE STUDY REVIEW TECHNOLOGY REQUIREMENTS RIA FITNESS PERFORMANCE USER Review of .See [Norwalk09] No user requirements -- straight to technological solution. Performance an afterthought. Quote .Box A good start is to not imagine what users want or need, but instead to talk with them about it. Try to walk in their shoes and understand how your software might help make their lives better (or not, as in this case). If you don't have time to do that yourself, then you should at least work with good product marketing people and listen to what they have to say. .Close.Box .Close ChungNixonYuMylopoulos99 .Open ChungNixonYuMylopoulos99 Lawrence Chung & Brian A Nixon & Eric Yu & John Mylopoulos Non-functional Requirements in software engineering Kluwer Acad Norwell MA 2000 ISBN 0-7923-8666-3 QA76.758 .N65 1999 =THEORY+CASESTUDYs FORMAL NFR SOFTGOALS SIGs GRAPHICS TABLES LOGIC QUALITIES REALITIES SYSTEMS TECHNIQUES Accuracy, security, performance, SIG:= "Softgoal Independency Graph", pp17+48+85 presenting arguments connecting statements independently of their (boolean) value: "dialectical style of reasoning". refinements and correlations {BREAK, HURT, UNKNOWN, HELP, MAKE}, AND, OR, EQUAL. denied, undecided, satisficed. Consolidates and summarizes: .See [MylopoulosChungNixon92] .See [BorgidaMylopoulosReiter93] .See [ChungNixonYuMylopoulos99] .See [MylopoulosChungYu99] .See [MylopoulosChungLiaoWangYu01] also see .See [Nixon00] .Close Church56 .Open Church56 Alonzo Church Introduction to mathematical logic: Volume I Princeton Univ Press 1956 No17 in Princeton mathematical series =TEXT LOGIC Skolem normal form in section 42 &43 .Close CimattiRoveriSusiTonetta12 .Open CimattiRoveriSusiTonetta12 Alessandro Cimatti & Marco Roveri & Angelo Susi & Stefano Tonetta Validation of Requirements for Hibrid Systems: A Formal Approach ACM TOSEM Trans Software Eng & Methodology V21n4(Nov 2012)#22:1-34 .See http://doi.acm.org/10.1145/2377656.2377657 =CASE STUDY UML OTHELLO ETCS LTL LINEAR TIME LOGIC TRAINS TOOLS ROSE SMT WORD Requisite Pro UML used to describe domain, a natural language form of LTL. Requirements classified: Glossary, Relationship, Action, Configuration, Behavior, Scenario, Property, Annotation. Formalized as UML class diagram plus LTL logic constraints. Tools check for consistency and completeness of requirements. Discover unexpected scenarios and cases where unwanted behaviors are allowed by the requirements. Example constraint for all t in trains .( in the future t.front.end != t.MA.EOA.location and .( in the future t.front.end = t.MA.EOA.location .) .) Experts learned to use the tools and method and liked them. .Close ClarkeEmersonSifakis09 .Open ClarkeEmersonSifakis09 Edmund M Clarke & E Allen Emerson & Joseph Sifakis Model Checking: algorithmic verification and debugging Commun ACM V52n11(Nov 2009)pp75-84 .See http://doi.acm.org/10.1145/1592761.1592781 =HISTORY MODEL CHECKING LTL CTL CTL* MODAL LOGICS PROOF TOOLS 2007 Turing Prize Article .Close ClarkeGrumbergPeled99 .Open ClarkeGrumbergPeled99 Edmund M Clarke Jr & Orna Grumberg & Doron A Peled Model Checking MIT Press 1999 ISBN 0-262-03270-8 QA 76.76 V47 C553 1999 =MONOGRAPH FORMAL LOGIC CTL MODEL CHECKING SMV SPIN OBDDS KRIPKE SYMMETRY GROUPS CSUSB cs565/656 .Close ClarkeRosenblum06 .Open ClarkeRosenblum06 Lori A Clarke & David S Rosenblum A Historical perspective on runtime assertion checking in Software Development ACM SIGSOFT Software Engineering Notes V31n3(May 2006)pp25-37 =HISTORY ASSERTIONS LOGIC PROVING DEBUGGING Ada Eiffel Anna C++ Euclid Turing Excellent bibliography on pages 34-37 .Close Cockburn96 .Open Cockburn96 Alistair Cockburn The 3 Rings of Object Technology Object Magazine (Nov 1996) pp20-22 DATA MODEL vs OBJECT-ORIENTED: structure vs changes. Modeling data on disk vs data in organization conceptual+logical+physical. Date model quicker. SCENARIOS:channel effort test completeness and variations. .See [CRC] encourages creativity. .Close Cockburn02b .Open Cockburn02b Alistair Cockburn Use Cases, ten years later STQE Magazine (Mar/Apr 2002) .See http://alistair.cockburn.us/Use+cases,+ten+years+later =HISTORY =HOWTO USE CASES FORMALLITY Brief Casual Fully dressed STAKEHOLDERS GOALS Theory .Set Use cases about one type of user and their goals -- the Prime Actor. Use cases are about the user's goals and the ways they try to fulfill these. Steps in scenarios achieve small goals on the way to a big goal. And Goals have different scopes/levels/sizes. Because there are actions that are invisible to the Prime Actor there must be other stakeholders involved with different interests. The Prime Actor want to get candy but the owner of the candy machine wants to get money for the candy... So there are contracts that the system must follow. There is more value in thinking out the alternative scenarios than the main success scenario. .Close.Set How people reacted to use cases... Some peole like formal structured use cases but others dislike them. Advice: Keep them simple. Keep them essential/logical. Use multiple formats: Brief, Casual, Fully Dressed. Mistakes: too many physical details, main use case too long and detailed. .Close CODASYL71 .Open CODASYL71 CODASYL Database Task Group CODASYL Database Task Group report ACM NY NY 1971 =STANDARD data logic ENTITIES SETS(FUNCTIONS) .Close Coen-Porisinietal91 .Open Coen-Porisinietal91 Alberto Coen-Porisini & Flavio De Paoli & Carlo Ghezzi & Dino Mandrioli Software Specialization Via Symbolic Execution IEEE Trans SE-17 n9 (Sep 1991)pp884-899 CR9302-0092 =DEMO logic symbolic execution re-engineering specialization .Close Cohen90 .Open Cohen90 Jacqes Cohen Constraint Logic Programming Languages Commun ACM V33n7(Jul 1990)pp52-68 =DEMO CLP non-sequential AI .Close CohenCampbell93 .Open CohenCampbell93 Donald Cohen & Neil Campbell Automating Relational Operations on Data Structures IEEE Software Magazine(May 1993)pp53-59 Example: topological sort on page 54 .Box do( x' in graph & no y in graph(y before x); out:!x; graph:~x; ) .Close.Box .Close Colmerauer90 .Open Colmerauer90 Alain Colmerauer An Introduction to Prolog III Commun ACM V33n7(Jul 1990)pp68-90 =LRM logic-programming non-sequential AI .Close Conallen99 .Open Conallen99 Jim Conallen(jconalle@Rational.com) Modeling web application architectures with UML Commun ACM V42n10(Oct 1999)pp63-70 in .See [Booch99] =ESSAY WWW/NET DESIGN UML stereotypes vs .See [RMM] Also see .See [Conallen98] on the WWW web application implement business logic and when accessed changes the state of the business. Separate business ADM from presentation UI. ADM:=Analysis/Design model classes: separate client side pages from server side pages. serverside builds clientside. components: Iconic stereotypes stereotypes for: server pages, client pages, links,builds, form, parts of forms, frame, target, applets, javascript, activex,... Details to be announced .See http://www.rational.com/ .Close ContedeLeonAlves-Foss06 .Open ContedeLeonAlves-Foss06 Daniel Conte de Leon & Jim Alves-Foss Hidden implementation dependencies in high assurance and critical computing systems IEEE Trans Software Engineering V32n10(Oct 2006)pp790-811 =CASE STUDY FORMAL HA&CCS ARTIFACTS RELATIONS LOGIC PROLOG GRAPHIC IMPLEMENTATION ABSTRACTION GUAM DO-178B Pedantic theory leads to tool that found problems in software from traceability relations on "work product sections" (artifacts). Translation into MATHS .Net artifact:Sets. implements: @(artifact,artifact) =given, indicates traceability between artifacts. |-STRICT_ORDER(strict_relation=>implements, artifact). l: artifact>->level =given, assigns a level to each artifact. <: @(level, level) =given. |-STRICT_ORDER(strict_relation=>(<), level). dependency: @(artifact, artifact) =goal. d := dependency. |- (conceptual_completeness): for x, y, z: artifact((if (x implements y and z) and l(x)<l(y)<l(z) then y d z) and (if (x and y implements z) and l(x)<l(y)<l(z) then x d y)) STRICT_ORDER::=http://csci.csusb.edu/dick/maths/math_21_Order.html#STRICT_ORDER .Close.Net .Close Cooke06 .Open Cooke06 John Cooke Constructing Correct software(2nd edn) Springer 2005 QA76.76 ISBN 1-85233-820-2 =INTRODUCTION MATHEMATICS LOGIC PROOF CORRECTNESS PROGRAMMING TECHNICAL compare with Bo Sandin's stuff in the 1980's and Huth & Ryan (textbook). .Close CookPodelskiRybalchenko11 .Open CookPodelskiRybalchenko11 Byron Cook & Andreas Podelski & Andrey Rybalchenko Proving program termination Commun ACM V54n5(May 2011)pp88-98 .See http://doi.acm.org/10.1145/1941487.1941509 =DEMO MATHEMATICS TERMINATION LOGIC DISJUNCTIVE Instead of proving that the transition relation R is a sub-relation of a well-founded relation T: R==>T, One can try to prove that R^(1..*) ==> | [i:1..n] T[i], where each T[i] is well-founded. Claims that "Ramsey's Theorem" implies that only a finite collection of T's need be considered. Adding extra statements and assertions to the code can express termination as invariants. For example, to verify that a variable is decreasing but positive: .As_is assert( oldx > x && x > 0 ); .As_is oldx:=x; Tools can then verify the invariants. Compare Andreas Blass and Yuri Gurevich. ACM Trans Comp Logic (Dec 2006) pp1-25 .See http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.146.4485&rep=rep1&type=pdf .Close Cousot90 .Open Cousot90 Patrick Cousot Methods and Logics for Proving Programs Chapter 15 (pp841..993) of Leeuwen90 =THEORY Operational and relational semantics .Box Studies relation between operational and relational semantics. Theorem 19(pages 856..858) proves that relational semantics imply operational with termination ignored. Angelic - Floyd non-determinsism and demonic - Dijkstra non-determinism being extreme cases in which operational can handle relational non-determinism. Refers to HoareLauer84, GreifMeyer81 .Close.Box .Close Cowanetal95 .Open Cowanetal95 Donald D Cowan & Carlos J P Lucena Abstract Data Views: An Interface specification Concept to enhance Design for Reuse IEEE Trans on Software Eng VSE-21n3(Mar 1995)pp229-243 CR9602-0126 =DEMO ADO ADV OBJECT-ORIENTED REUSE ARCHITECTURE .Box ADO - Abstract Data Object Rediscovering the value of separating the physical from the logical and one type of object from another, also from network... .As_is I/O ADO .As_is \ / || .As_is ADV1 ADV2 MVC suggests use of dynamic objects! ADV2 are relations! Claims OMT is an modernized version of JSD!(RUBBISH) Quotes Kazman et al: Metaphors as first class objects. Reccommends developing graphic notations .Close.Box .Close CrowVito98 .Open CrowVito98 Judith Crow & Ben Di Vito Formalizing Space Shuttle Software Requirements: Four CASE Studies ACM TOSEM V7n3(Jul 1998)pp215-249 =ANALYSIS EXPERIENCE .See [PVS] GPS RAPID FORMAL LOGIC TABLE MATH Mur\Phi .Box Where do states come from, shared variables used as input/output. Large number of errors discovered (early) just by formalizing requirements without checking! Need for readymade math theories: eg properties of mappings! Failed proofs are more help than successful ones. Specification is iterative. Need to specify constraints found in the problem domain. Can simplify model: remove continuous values and time and remove costraints. Therefore check some impossible states Tailor formal methods to the situation. .Close.Box .Close DalaKamathKolarikSivaraman04 .Open DalaKamathKolarikSivaraman04 Nikuni P Dala & Manjunath Kamath & WilliamJ Kolarik & Eswar Sivaraman Toward an Integrated Framework for Modeling Enterprise Process Commun ACM V47n3(Mar 2004)pp83-86 =ADVERT BUSINESS PROCESS MODELLING IMPROVEMENT ERP EPML XML Petri Analysis TED Need to model/implement distributed. Need for process semantics. Need to link business and enginering. Graphic front-end($EPML) <->XML<-> formal Back-end. Analise back end. NSF Scalable Enterprise Systems Initiative. EPML::="Enterprise Process Modelling Language". Graphic showing: activities (Human, Computer, Machine), logic and decision logic, data icons, control flows , (input, output)><( material, data), timing triggers. TED::="Task Execution Diagram". Analysis petri nets: design (termination, deadlock, safety) + performance (resource assignment, simulation, timing, success vs time statistics) .Close DanforthTomlinson88 .Open DanforthTomlinson88 S Danforth & C Tomlinson Type Theories and Object Oriented Programming Comp Surveys V20n1 (pp29-72)Mar 1988 =THEORY object-oriented logic Reality .Close Date00 .Open Date00 Christopher J Date What not how: the business rules approach to application development Addison-Wesley Longman Boston MA 2000 pp131 $24.95 ISBN 0-201-70850-7 CR0011-0557 H.2.0 qa76.76 a65 d375 2000 =ADVERT RULES SQL LOGIC LPC TABLES .Close DeBakker75 .Open DeBakker75 J W de Bakker Flow of Control in the Proof of Sequential Programs Proc 16th Ann Symposium on the Fundamentals of Computer Science Berkeley California(pp29-33) IEEE Computer Society 1975 =THEORY regular logic .Close DeganoEtAl08 .Open DeganoEtAl08 Pierpaolo Degano & Rocco De Nicola & Jose Meseguer (eds) Concurrency, Graphs and Models: Essays dedicated to Ugo Montanari on his 65th Birthday LNCS 5065 Springer Verlag Berlin Heidelberg (2008) $CR 0909-0812 =FESTSHRIFT MATHEMATICS GRAPH THEORY CONCURRENCY NON-SEQUENTIAL CATEGORIES SEMIRINGS TOOLS HISTORY Includes .See [AstesianoReggioRicca08] UML BUSINESS ... .See [Baetan08] ALGEBRA EQUATIONS AUTOMATA ... .See [BeauxisPalamidessiValencia08] NONSEQUENTIAL BAGS... .See [HermenegildoEtAl08] LANGUAGE Ciao ... .See [Quaglia08] BIOLOGICAL CELLULAR SYSTEMS... .Close Delgrande98 .Open Delgrande98 James P Delgrande(Simon Fraser U, Burnaby, BC, Canada)<jim@cs.sfu.ca> On first-order conditional logics Artif Intell V105n1-2(Oct 1998)pp105-137 CR9903-0211 =THEORY defeasible LOGIC possible worlds Kripke .Box Proposes replacing `for all x( P implies_if_normal Q)` by `P implies_for_all_normal[x] Q` Examples: all birds fly, penguins are birds, penguins don't fly. All elephants like their keepers, unless the keeper is mean like Fred in which case they don't like him, unless the elephant is Clide who likes all the keepers. .Close.Box .Close DeLine01 .Open DeLine01 Robert DeLine Avoiding Packaging Mismatch with Flexible Packaging IEEE Trans Software Engineering V27n2(Feb 2001)pp124-143 in ICSE'99 + Correction IEEE Trans Software Engineering V27n6(Jun 2001)p576 =DEMO MODULE ARCHITECTURE ware+packager NONSEQUENTIAL Allows one piece of logic to be mapped into spreadsheet, CGI, yacc, .... Stresses use of coroutines as more flexible than procedural code. .Close DeMilloLiptonPerlis79 .Open DeMilloLiptonPerlis79 Richard DeMillo & Richard Lipton & Alan Perlis Social processes and Proofs of Theorems and Programs Commun ACM V22n5(May 1979) pp271-280, letters V22n11pp621-630 =ESSAY EXAMPLES MATHEMATICS PROOF LOGIC p272: "There is simply no way to describe the history of mathematical ideas without describing the successive social processes at work on proofs." See .See [Lakatos76] .See [Bauer92] (DeMilloLiptonPerlis79)|- `rigorous software development will also depend on social processes` .Close DeMouraBjorner11 .Open DeMouraBjorner11 Leonardo de Moura & Nikolaj BjC8rner Satisfiability modulo theories: introduction and applications Commun ACM V54n9(Sep 2011)pp69-77 .See http://doi.acm.org/10.1145/1995376.1995394 =ADVERT LOGIC FORMAL MATHEMATICS PROBLEM SOLVING TOOLS SMT SAT SMT solve problems within specialized mathematical theories. Example theory: difference arithmetic where every formula has form `x-y<=c` where `x` & `y` are variables and `c` is a constant. SMT work with SAT solvers. Several solvers for different theories can be combined. Many problems about programs can be expressed in the theories with tractable solvers. .Close DeneckerBruynooghe02 .Open DeneckerBruynooghe02 Marc Denecker & Maurice Bruynooghe Logic Programming Revisited: Logic Programs as Inductive Definitions ACM Trans Computational Logic V2n4(Oct 2001)pp623-654 =THEORY LOGIC Prolog INDUCTION .Close Denning94 .Open Denning94 Peter J Denning Designing a Discipline of Software Design Keynote address at the 7th SEI Conference on Software Engineering Education "Putting the 'Engineering' into Software Engineering" January 5-7 1994 San Antonio Texas USA =IDEA REALITY ONTOLOGY .See [WandWeber90] cf .See [WiederholdWegnerCeri93] cf ?? S-->RPQ->T (ontological mapping) .Box From Abstract The central claim explored here is that the standard engineering design process produces a fundamental blindness to the domains of action in which the customers of software systems live and work. The connection between measurable properties of the software and the satisfaction of those customers is, at best, tenuous. We propose a broader interpretation of design that is centered on observing the work processes of a community of customers in a domain and connecting those processes to supportive software technologies. The skill that a designer needs to have to observe work processes and begin making the connections is here called `ontological mapping`. This skill can be learned and is the basis of a discipline of software design. .Close.Box .Close DenningHorning0202 .Open DenningHorning0202 Peter J Denning & James J Horning Inside RISKS: Risks of Linear Thinking Commun ACM V45n2(Mar 2002)p120 =ESSAY USER vs TECHNIQUE Quotes Donald Stokes (Pasteur's quadrant: basic science and technological innovation, Brooking's institute, 1997). 2><2: inspired by use >< quest for fundamental understanding. Pasteur(Y,Y), Bohr (N,Y), Edison(Y,N), and unnamed(N,N). Argues that software development is similar: focus on the user and focus on the technical aspects. .Close DesaiEtal05 .Open DesaiEtal05 Nirmit Desai & Ashok U Mallya & Amit K Chopra & Munindar P Singh Interaction protocols as design abstractions for business processes IEEE Trans Software Engineering V31n12(Dec 2005)pp1015-1027 =THEORY MODEL BUSINESS PROCESS COMMITMENTS SCENARIOS OWL-P AGENTS ROLES \pi-CALCULUS Proposes a logic of commitments between agents. Uses sequence charts containing commitments to describe protocols. Implies that activity diagrams are a bad way to describe business processes. Entangles the internal logic of different agents with each other. So unstable. (dick)|- `take home message: don't use control flows to model work flow`. .Close DesaiChopraSingh09 .Open DesaiChopraSingh09 Nirmilt Desai & Amit K Chopra & Munindar P Singh Amoeba: A methodology for modeling and evolving cross-organizational business processes ACM Transactions on Software Engineering and Methodology V19n2(Oct 2009)pp6.1-45 =ADVERT 2 CASE STUDIES Amoeba REQUIREMENTS METHOD LOGIC COMMITMENTS SCENARIOS SEQUENCE CHARTS AXIOMS EVOLUTION AGENTS SERVICES ORCHESTRATION CHOREOGRAPHY Amoeba::Method= iterate( roles and interactions; contractual relationships -> Commitments; message meanings->create and manipulate commitments; Constraints; compose protocols -> process model). Uses the idea of .Key business protocols as modules. These have messages and resulting changes in the commitments between components. For example `CC(VENDOR, BUYER, pay(price), ship(goods))` would result from a VENDOR sending a `quotation(price, goods)` message to a BUYER. Theory .See [DesaiEtal05] .Close Deville90 .Open Deville90 Yves Deville Logic Programming: Systematic Program Development Addison Wesley 1990 QA76.63.D48 CR9204-0201 & CR9102-0042 =TEXT LOGIC PROGRAMMING .Box Note pp14-17 outlines steps: Problem->Spec(predicates, multiplicity and directionallity)->first order logic->logic program. (MATHS suitable for expressing the Problem and perhaps the Spec as well.) .Close.Box .Close Dijkstra76 .Open Dijkstra76 Edsger W Dijkstra A Discipline of Programming Prentice Hall Inc Englewood Cliffs NJ =TEXT guarded-commands sequential non-sequential formal logic structures .Close Dijkstra89 .Open Dijkstra89 Edsger W Dijkstra On the Cruelty of Really Teaching Computer Science Talk at ACM Computer Science Conference Louisville Feb 1989(See .See [Denning89b] ) =TALK formal logic education .Close DilligDilligAiken10 .Open DilligDilligAiken10 Isil Dillig & Thomas Dillig & Alex Aiken Reasoning about the unknown in static analysis Commun ACM V53n8(Aug 2010)pp116-123 .See http://doi.acm.org/10.1145/1787234.1787259 =DEMO LOGIC MATHEMATICS MODEL CHECKING C Linux may/must SOUNDNESS .Close Dillonetal94 .Open Dillonetal94 Laura K Dillon & G Kutty & L E Moser & P M Melliar-Smith && Y S Ramakrishna A Graphical Interval Logic for Specifying Concurrent Systems ACM Trans Softw Eng Methodol V3n2(Apr 1994)pp131-165 .See http://citeseer.nj.nec.com/33145.html .See http://portal.acm.org/citation.cfm?id=192218.192226&coll=portal&dl=ACM&idx=J790&part=transaction&WantType=transaction&title=ACM%20Transactions%20on%20Software%20Engineering%20and%20Methodology%20%28TOSEM%29&CFID=1643654&CFTOKEN=8691090 =ADVERT NOTATION MODAL TEMPORAL LOGIC FORMAL GIL TOOL GILED GIL::="Graphic Interval Logic". Later see .See [RTGIL] -- real time GIL .Close DjuricDevedzic10 .Open DjuricDevedzic10 Dragan Djuric & Vladan Devedzic Magic Potion: incorporating new development paradigms through metaprogramming IEEE Software Magazine V27n5(Sep/Oct 2010)pp38-44 =ADVERT JAVA LISP JVM Modeling Spaces XML RDF/OWL DSL DOMAIN MODEL LOGIC ONTOLOGY UML MDA Clojure::=http://clojure.org, Dialect of LISP that runs in the Java Virtual Machine. .Close Doernhoefer06a .Open Doernhoefer06a Mark Doernhoefer Surfing the Net for Software Engineering Notes: Requirements Management ACM SIGSOFT Software Engineering Notes V31n2(Mar 2006)pp17-25 .See http://doi.acm.org/10.1145/1118537.1118553 =SURVEY NET REQUIREMENTS Excellent survey of resources on the web .See http://www.jiludwig.com/ .See http://cio.doe.gov/ITReform/sqse/requirements_management.htm .See http://www.goldpractices.com/practices/mr/index.php .See http://www.sei.cmu.edu/str/descriptions/reqtracing.html .See http://www.agilealliance.com/articles/AgileArticlesCatSearch?category=Requirements .See http://www.paper-review.com/tools/rms/read.php (tools) .See http://www.opengroup.org/architecture/togaf8-doc/arch/p2/p2_req.htm .See http://www.rallydev.com/life_cycle_management.jsp .See http://www.erequirements.com/app?service=page/Methodology .See http://www-306.ibm.com/software/rational/offerings/reqanalysis.html .See http://www.telelogic.com/ .See http://www.iceincusa.com/16CSP/content/8_requir/reqfrm.htm plus lots more... .Close Doernhoefer09c .Open Doernhoefer09c Mark Doernhoefer Surfing the net for software engineering notes: computer science ACM SIGSOFT SEN V34n5(Sep 2009)pp8-17 .See http://doi.acm.org/10.1145/1598732.1598752 =SURVEY SWEBOK SigACT ALGORITHMS CALGO NUMERICAL NIST GAMS DATA STRUCTURES THEORY HARDWARE TM OS IMBOK FUZZY LOGIC PROGRAMMING LANGUAGES .Close Douglass99 .Open Douglass99 Bruce Powel Douglass Components: Logical, Physical Models Software Development Magazine V7n12(Dec 1999)pp52-54 =ADVERT OBJECT-ORIENTED METHOD UML ROPES COMPONENTS Components are runtime plugin Binaries not objects .Note UML components include data files, web pages, source code, etc etc. .Close DutertreStavidou97 .Open DutertreStavidou97 Bruno Dutertre & Victoria Stavidou Formal Requirements Analysis of an Avionics Control System IEEE Trans Softw Eng VSE23n5(May 1997)pp267-278 =DEMO V&V REQUIREMENTS LOGIC TOOLS TIMING RISKS REALITY PVS .See [PVS] model of time and clocks exposed some unstated assumptions about REALITY and one defect .Close DuvalHodgins06 .Open DuvalHodgins06 Erik Duval & Wayne Hodgins Standardized Uniqueness: Oxymoron or Vision of the Future IEEE Computer Magazine V39n3(Mar 2006)pp96-98 =STANDARD EDUCATIONAL OBJECTS METADATA LOM IEEE1484 LTSC XML The IEEE1484 standard specifies the information to be recorded about "Learning Objects": artifacts that help you learn. The standard is MODULAR separating logical structure from physical bindings. The standard defines many data elements in a hierarchical data model but every part is optional. How to make the metadata invisible? .Close EdwardsJacksonTorlak04 .Open EdwardsJacksonTorlak04 Jonathan Edwards & Daniel Jackson & Emina Torlak A Type System for Object Models Proc SIGSOFT'04/FSE-12& ACM SIGSOFT Software Engineering Notes V29n6(Nov 2004)pp189-199 =IDEA LOGIC RELATIONAL TYPES Alloy 2.0 Defines an improved type system for Alloy with subtypes, relations, etc. Compares with UML OCL. Precisely defines two types for formulas: bounding type and relevance type. An empty relevance type indicates an error. .Close Eisenstadt97 .Open Eisenstadt97 Marc Eisenstadt My Hairiest Bug War Stories Comm ACM V40n4(Apr 1997)pp30-37 CR9711-0918 =POLL RISKS QUALITIES DEBUGGING Very interesting. Internet POLL for bugs classified for difficulties(long cause-effect chain and hampered tools being commonest) + how found(gathered data and ispeculation leading) + root cause(memory, vendor, design,logic, initialization ...) +interaction(use data gathering when cause-effect chain is likely to be long or the tools are hampered) .Close EmmerichEtal99 .Open EmmerichEtal99 Wolfgang Emmerich & Anthony Finkelstein & Carlo Montangero & Stefano Antonelli & Stephen Armitage & Richard Stevens Managing Standards Compliance IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp836-837 =THEORY MODEL LOGIC FLEA TOOL DOORS DXL STANDARDS in PROCESS uses STATECHART UML~OCL+1st_order_logic PETRI Net LISP (AP5) FLEA::="Formal Language for Expressing Assumptions". .Close Engelsetal92 .Open Engelsetal92 G Engels & C Lewerentz & M Nagl & W Schafer & A Schurr Building Integrated S Development Environments Part 1: Tool Specification ACM Trans Softw Eng Methodol V1n2(Apr 1992)pp135-167 .Box IPSEN(Integrated Project Support Environment) PROGRESS Attributed Graphs visual data base CFG+CS rules on attributes in graph, object oriented is-a, prime as new node, Path expressions, atomic transactions, Factoring out common rules, logical vs representation graph. .Close.Box .Close Epstein94 .Open Epstein94 Richard L Epstein The Semantic Foundations of Logic: Predicate Logic Oxford U Press Inc NY NY ISBN 0-19-508760-7 CR9601-0018 philosophical translation of Natural language into various predicate calculi .Close Epstein01a .Open Epstein01a Richard L Epstein Predicate logic: The semantic foundation of Logic Wadsworth Belmont CA 2001 ISBN 0-534-55846-1 BC181.E67 2001 $40.95 pp412 CR0011-0555 F.4.1 =TEXT =REFERENCE LOGIC PC MODAL `x is a dog` notation! CSUSB CS556/656 .See [Epstein94] .Close Epstein01b .Open Epstein01b Richard L Epstein Propositional logic: The semantic foundation of Logic Wadsworth Belmont CA 2001 ISBN 0-534-55846-1 BC181.E67 2001b =TEXT =REFERENCE LOGIC PC MODAL CSUSB CS556/656 .Close Epstein06 .Open Epstein06 Richard L Epstein Classical mathematical logic: The semantic foundation of Logic Princeton UP Princeton NJ 2006 ISBN 0691123004 $CR 0803-0245 =UNREAD =TEXT =REFERENCE LOGIC Compare .See [Epstein01b] .See [Epstein01a] .See [Epstein94] .Close Farmer03 .Open Farmer03 William M Farmer A Basic Extended Simple Type Theory McMaster University Hamilton Ontario CA (29 Sep 2003) =IDEA LOGIC TYPES BESTT ::= $CSTT with HOL, sets, lists, & tuples. CSTT ::= Church's Simple Type Theory. .Close FarmerMohrenschildt00 .Open FarmerMohrenschildt00 William M. Farmer and Martin v. Mohrenschildt Transformers for Symbolic Computation and Formal Deduction Presented at a Workshop on the Role of Automated Deduction in Mathematics, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 2000 .See http://imps.mcmaster.ca/doc/transformers.pdf =IDEA LOGIC DEDUCTION COMPUTATION TERM TRANSFORMERS STTM::="von-Neumann-Bernays-Goedel set theory". This has terms and formulas. Terms may be undefined, but formulas are always defined and are either true or false. Transformers are total functions which may or may not preserve meaning or logistic properties like being (provably) true or false. .Close Felderetal94a .Open Felderetal94a Miguel Felder & Dino Mandroli & Angelo Morzenti Proving Properties of Real-Time Systems Through Logical Specifications and Petri Nets IEEE Trans SE V20n2(Feb 1994)pp127-141 =FORMAL TIMING Temporal TRIO .Box Basic temporal operator Dist( P, d ) ::=`P is true d time units from (_)`, model of timed petrie nets proof that dining philosphers TPN is deterministic and every body eats every 7 units of time! compare with MATHS manual on Modal Logic Question: They prove a liveness property of the philosophers by proving a liveness property for one fork. Is this circular? .Close.Box .Close Felderetal94b .Open Felderetal94b Miguel Felder & Angelo Morzenti Validating Real-Time systems by History-Checking TRIO Specifications Trans Softw Eng Methodol V9n4(Oct 1994)pp308-339 =EXPERIENCE TIMING TRIO LOGIC SPECIFICATION PROOF .Box Some experiences with Italian utility companies Semantic tableaus for proof and for history checking Futr(A,t) ::=A(_+t), Past(A,t) ::=A(_-t) Table 1, p316 defines: AlwF, AlwP, Alw, SomF, SomP, Som,Lats,Lasted, since, Since[w], WithinP, Until, Until[w], UpToNow, FirstTimeF .Close.Box .Close FeltyNamjoshi03 .Open FeltyNamjoshi03 Amy P Felty & Kedar S Namjoshi Feature Specification and automated Conflict Detection ACM TOSEM Trans Software Eng & Methodology V12n1(Jan 2003)pp3-27 =CASESTUDY telecommunications SPECIFICATION FEATURES LOGIC LTL FSM Buchi MODEL Checking TOOL FIX COSPAN Features expressed in sugared LTL: pre/post conditions. including until/unless discharge requirements. Complex/careful definition of what it means for two features to conflict. FIX use LTL approximation to find witnesses for conflicts. .Close FerrariGnesiMontanariPistore03 .Open FerrariGnesiMontanariPistore03 Gian-Luigi Ferrari & Stefania Gnesi & Ugo Montanari & Marco Pistore A Model-Checking Verification Environment for mobile Processes ACM TOSEM Trans Software Eng & Methodology V12n4(Oct 2003)pp440-473 =DEMO TOOL MODEL CHECKING MOBILE \pi-calculus FSM HD-Automata HAL \pi-logic ACTL .Close FeysFitch69 .Open FeysFitch69 RObert Feys & Frederic B Fitch Dictionary of Symbols of Mathematical Logic Amsterdam North-holland Pub Co 1969 =DICTIONARY LOGIC SYMBOLISM LANGUAGE .Close FilipenkoMorris92 .Open FilipenkoMorris92 I Filipenko & F L Morris Domains for Logic Programming Theor Comput Sci V94n1(Mar 1992)pp63-99 CR9304-0239"Original and sound" .Close Finkelsteinetal94 .Open Finkelsteinetal94 Anthony C W Finckelstein & Dov Gavey & Anthony Hunter & Jeff Kramer & Bashar Nuseibeh Inconsistency Handling in Multiperspective Specifications IEEE trans on Soft Eng vSE-20n8(Aug 1994)pp569-578 =IDEA REQUIREMENTS LOGIC SPECIFICATION See Nuseibehetal94 .Box VeiwPoint::=Net{Style, Work_Plan, Domain, Specification, Work_Record}. .Close.Box .Close Firesmith93 .Open Firesmith93 Donald G. Firesmith Object-oriented Requirements analysis and logical design: A software engineering approach John Wiley & sons NY NY 1993 ISBN 0-471-57807-X CR9502-0058 .Close FittingMendelsohn98 .Open FittingMendelsohn98 Melvin C. Fitting and Richard Mendelsohn First-Order Modal Logic Kluwer 1998 paperback 1999 =TEXT FORMAL LOGIC MODAL THEORY Modal predicate logic .Close Floyd67a .Open Floyd67a Robert W Floyd Assigning Meaning to Programs pp19-32 of Proceedings of Symposia in Applied Mathematics Vol XIX formal logic PROOF .Close Fowler01c .Open Fowler01c Martin Fowler Separating User Interface code IEEE Software Magazine V18n2(Mar/Apr 2000)pp96-97 =ESSAY MODULES USER REALITY XML SQL HTML p.96: ` Separate presentation code from domain code.` increases maintainability, portability, testing. Problems: VB, Delphi,... don't do this. WEB server pages that contain business logic. HTML vs XML. .Close Fox66 .Open Fox66 Fox(Ed) Advances in Programming & Non-Numerical Computation Pergamon Press Oxford UK =SURVEY formal logic .Close Francez86 .Open Francez86 Nissim Francez Fairness Springer Verlag NY NY 1986(Texts & Monographs in Comp Sci). ISBN 0-387-96235-2 (UCR) QA76.6.F7226 ACM(D.1.3 D.2.4 D.3.1 D.4.1 F.1.2 F.3.1 F.3.3) termination safety liveness temporal logic .Close Fraseretal94 .Open Fraseretal94 Martin D Fraser & Kuldeep Kumar & Vijay K Vaishnavi Strategies for Incorporating Formal Specifications in Software Develpment Commun ACM V37n10(Oct 1994)pp74-86 CR9509-0705 .Box Note -- quotes examples limitted to VDM+XYZ Footnote 1: Specification in terms of system components, options,... vs Spec as callection of user's "functional requirements" p75: past research has focussed on notation and rules of inference not on methods and tools, "The Softaware engineer is lef to his or her own devices to discover the software requiements and structure them into a requirements architecture." p75: Most need discrete math and logic which most SwEngs don't know. Table 1 Page77: defines methods, lists 10: VDM, Z, Larch, FSM, Petri Nets, Temporal Logic, Transition Axioms, CSP, CCS, PAISLEY Page 78. Lists 9 strategies of use Table 2, page 79: informal vs semi-formal vs formal: definition and examples (JSD as semiformal) Morphological analysis Table 3: Formalization Processes (taxonomy= { direct, transitional={sequential, parallel}}) Table 4: Support: Unassistted vs Computer Assisted Table 5: Table 3 >< Table 4 -> references 25 refs .Close.Box .Close Freedman83 .Open Freedman83 Roy S Freedman The Common Sense of Object Oriented Languages Computer Design pp111-118 structures object-oriented logic .Close FreydScedrov89 .Open FreydScedrov89 Pete J Freyd & Andre Scedrov Categories& Allegories Elsevier Amsterdam Netherlands ISBN0-444-70368-3 QA169.F73 allegories are abstracted from binary relations like categories abstracted from functions notation for diagrams: noncommuting (+) + pullbacks + equalizers + products quantification based on making visible the comments(quantiviers and logical connectives) made while drawing the diagram on a blackboard .Close FriasEtal05 .Open FriasEtal05 Marcello F Frias & Carlos G Lopez Pombo & Gabriel A Baum & Nazareno M Aguirre & Thomas S E Maibaum Reasoning about static and dynamic properties in Alloy: A Purely Relational Approach ACM TOSEM Trans Software Eng & Methodology V14n4(Oct 2005)pp478-526 =THEORY EQUATION RELATIONAL LOGIC HOARE TRIPLES FORK ALGEBRA FRL A .Key fork algebra is based on a set that has a pairing operation (`p`) that is used to define a `fork` operation on relations: fork ::infix=map[R,S] rel[a,d](for some b,c (d=p(b,c) and a R b and a S c)). .Close GanterWille99 .Open GanterWille99 Bernhard Ganter & Rudolf Wille R Formal concept analysis: Mathematical foundations Springer 1999 QA171.5 G3513 1999 =THEORY MATHEMATICAL FORMAL LOGIC LATTICE CONCEPT Given a set of objects X, a set of attributes Y, and a relation R:@(X><Y), then (X,Y,R) is called a formal context. If A is a subset of X then define A'={y:Y. for all x:A(x R y)}. Similarly B'={x:X.for all y:B( x R y)}. A formal concept is a pair (A, B) where A'=B and B'=A, and A is the extent and B the intent of concept (A,B). The subconcept_superconcept relation:(A1,B1) <= (A2,B2) iff A1 is a subset of A2. This defines a lattice of formal concepts. Leads to a diagram showing the underlying structure of the relation R. Given a table X><Y<>-> Z and by defining a scaling Z into (true, false) then a context can be defined. See .See http:://www/dick/maths/logic_42_Properties_of_Relation.html for some rough notes on Concept analysis. Note. Theory has been used to aid the maintenance of software: .See [BojicVelasevic00] .See [DeursenKuipers99] .See [LindigSnelting97] .See [SiffReps99] .See [Snelting96] .See [SneltingTip98] .Close GaoHayesCai05 .Open GaoHayesCai05 Hong Tina Gao & Jane Huffman Hayes & Henry Cai Integrating Biological Research through Web Services IEEE Computer Magazine V38n3(Mar 2005)pp26-31 =DEMO WEB SERVICES BIOINFORMATICS Drug discovery Combine many remote components to analyze data. Need standards. Helps if people split Model from View. .Close Garfinkel05 .Open Garfinkel05 Simson Garfinkel Microsoft's Secret Bug Squasher Wired (Nov 10 2005) .See http://www.wired.com/news/technology/bugs/0,2924,69375,00.html?tw=wn_tophead_3 =REPORT MS MODEL CHECKING DEVICE DRIVERS TOOL SLAM So called `formal methods` -- math & logic -- are used inside Microsoft! .Close GargantiniMorzenti01 .Open GargantiniMorzenti01 Angelo Gargantini & angelo Morzenti Automated Deductive Requirements analysis of Critical systems ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp255-307 =DEMO FORMAL REQUIREMENTS ANALYSIS SRA LOGIC .See [TRIO] TD TOOL PVS Non-Zeno TD:="Time dependent". TRIO -- see Federer DUC::="Device under Construction". events (point based predicates) : true at a single time and not immediately before or after. interval-Based predicates: if true then true in some before or after interval nearby and if false then false nearby.. left and right closed interval-based predicates and variables. Left continuous interval based (lci) means that predicate has the same value at a given time as it had in a previous neighboring interval. non-Zeno predicates and variable. Named after Zeno's paradoxes. finite variability. physical meaningful. One can talk about the value immediately before or after the current time. non_Zeno(A) ::=(UpToNow(not A) or UpToNow(A)) and (NowOn(not A) NowOn(A) ), UpToNow(A) ::= t+>for some d1>0, all d2:(0..d1) ( A (t-d2)), NowOn(A) ::= t+>for some d1>0, all d2:(0..d1) ( A (t+d2)) .Close GeethaSubramanian90 .Open GeethaSubramanian90 T V Geetha & R K Subramanian Representing Natural Language with Prolog IEEE Software V7n2 pp85-92 =ADVERT DDD LOGIC PROLOG LANGUAGE NLP .Close GervasiNuseibeh02 .Open GervasiNuseibeh02 Vincenzo Gervasi & Bashar Nuseibeh Lightweight validation of natural language requirements Software - Practice & Experience V32n2(Feb 2002)pp113-133 =CASESTUDY LITE FORMAL V&V REQUIREMENTS LOGIC NASA Shows how lightweight formalism can find errors in natural language specifications. This is easy and not expensive, and finds subtle errors. .Close GiannakopoulouMagee03 .Open GiannakopoulouMagee03 Dimitra Giannakopoulou & Jeff Magee Fluent Model Checking for Event-based systems FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp257-266 =THEORY TOOL TEMPORAL LOGIC V&V LTS LTL FLUENT FLTL LTSA Buchi A fluent is a property of states defined by events at the start and end. Example TUNING starts when the tuner is turned on and ceases when the device is tuned in. Syntax: <start_set, end_set> initially (true|false). Define shorthand for fluents for single actions/sets of actions: <S, All~S>initially false. .Close Gilb96 .Open Gilb96 Tom Gilb(gilb@acm.org) Level 6: Why we Can't Get There From Here IEEE Software Magazine V13n1(Jan 1996)pp97-98+103 =ADVERT QUALITY evolutionary delivery engineering Softcrafters .Box Quotes Biily Koen(U of Austin TX) : "Engineering is the use of principles to find designs that will meet multiple competing objectives within limited resources and other constraints, under conditions of uncertainty". Platitudes instead of quantitive specs make engineering logically impossible. .Close.Box .Close GilmoreTsiknis93 .Open GilmoreTsiknis93 Paul C Gilmore & George K Tsiknis(UBC) A Logic for Category Theory Theor Comput Sci V111n1-2(Apr 1993)pp211-252 CR9409-0647 .Box CR(T H Tse) : Natural deduction based set theoretic semantics for categories - using joint denial and universal quantification as primitive... Tarski semantics... categories & Functiors... avoids paradoxes but permits selfmembership (eg category of categories is a category!)...remarkable. some doubts. .Close.Box .Close GortonLiuBrebner03 .Open GortonLiuBrebner03 Ian Gorton & Anna Liu & Paul Brebner Rigorous Evaluation of COTS Middleware Technology IEEE Computer Magazine V36n3(Mar 2003)pp50-55 =DEMO QUALITIES WEB/NET Java J2EE servers MTE WebSphere WebLogic ... .Close Gries91 .Open Gries91 David Gries Teaching Calculation and Discrimination: A More Effective Curriculum Commun ACMV34n3(Nar 1991)pp44-54. Letters Commun ACM V34n9(Oct 1991)pp16-18 & 91-95 & Commun ACM V35n2(Feb 1992)pp22-26 =ESSAY FORMAL LOGIC MATH EDUCATION .Box text book version .See [GriesSchneider93] p45"In Summary, Software engineering, Computing, and Computing education all suffer from a lack of basic mathematical skills that are needed in dealing with algorithmic concepts.", "Calculational proofs", "overhauling the CS Magor", p54"The main activity that is supposed to separate engineering from other fields is design: the actual activity of preparing a plans for some object[..] design of proofs[...]". p54"Let us all learn more about calculational techniques and gain skill with them: and let us begin to teach computing using them." .Close.Box .Close Gries96 .Open Gries96 David Gries(mailto:gries@cs.cornell.edu) The Need for Education in Useful Formal Logic IEEE Computer Magazine V29N4(Apr 1996)pp29-30 .Box Logic as a tool. calculational proofs logic is a tool not a panacea .Close.Box .Close GriesSchneider95 .Open GriesSchneider95 David Gries & Fred B Schneider Teaching Math More Effecively Through Calculational Proofs Am Math Monthly V102n8(Oct 1995)pp691-697) =ADVERT CALCULATIONAL LOGIC MATHEMATICS Advert for .See [GriesSchneider93] .Box 15 axioms and 4 rules = is transitive, can substitute a free variable, equanimity: if P and (P \equiv Q) then Q and Liebnitz: .Box E[v:=P] = <P=Q> E[v:=Q] .Close.Box Where P and Q are expressions and v some variable not found in P or Q and E[v:=P] some expression with every ovccurrence of v replaced by P and E[v:=Q] the same expression with every v replaced by Q. Also treats \equiv as an associative (serial) operator, and equals as a parallel operator. Unified notation for all quantification, summation, etc: (op var | condition : expression) Formal notation is a repository of facts and a means of clarification. It provides rules for judging the soundness of inference and detecting and eliminating ambiguity. .Close.Box .Close Grossman11 .Open Grossman11 Lisa Grossman Study: Math Skills Rely on Language, Not Just Logic Wired Science (Feb 8 2011) .See http://www.wired.com/wiredscience/2011/02/homesigning-numbers/ =REPORT EXPERIMENT SIGNERS NUMBERS COUNTING ARITHMETIC PEOPLE PSYCHOLOGY This reports on a recent experiment in Nicuagua by Elizabet Spaepen. It shows that if you don't know the words for the numbers you can not communicate a number (as in the number of sheep) correctly. Memorizing the mnemonic sequence (one,two, three, ...) provides pegs to hang observations on... .Close Grunske08 .Open Grunske08 L Grunske Specification patterns for probabilistic quality properties ACM/IEEE 30th Conf ICSE'08 Software Engineering(May 2008)pp31-40 =THEORY =DEMO PROBABILISTIC VERIFICATION QUALITIES PCTL* CSL TEMPORAL LOGIC ProProST PATTERN LANGUAGE STRUCTURED ENGLISH GRAMMAR English Subset .See ./samples/Grunske08.html grammar. .Close Guerevich87 .Open Guerevich87 Yuri Guerevich Logic and the Challenge of Computer Science pp1-57 in Borger88 .Box Note "For years formal languages were in the private domain of logicians. But what formal language is most popular today?[...] The most popular formal languages are programming languages. Another kind of popular formal languages are database query languages. Some other formal languages emerge in artificial intelligence like languages for knowledge representation. Old discussions on names, denotations, types, etc. are suddenly revitalised to unprecedented magnitude"(p1),"no first order formula \phi expresses on finite graphs that (x,y) belongs to the transitive closure of the edge relation"(pp3-4). .Close.Box .Close Gumb89 .Open Gumb89 Raymond D Gumb Programming Logics: An Introduction to Verification and Semantics John Wiley & Sons NY NY 1989 natural deduction introduction to hoare axioms and dentational semantics .Close Gurevich88 .Open Gurevich88 Yuri Gurevich Logic and The challenge of Computer Science in .See [borger88] =THEORY FORMAL LOGIC COMPUTING .Close GurfinkelDevereuxChechik02 .Open GurfinkelDevereuxChechik02 Arie Gurfinkel & Benet Devereux & Marsha Chechik Model Exploration with temporal logic query checking SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp139-148 =DEMO TOOL MODEL CHECKING CTL QUERIES Given a finite state model enable the faster answering of questions like: what property is always true with `p`. Cruise control example. refers to Chan's original idea. Developed to .See [GurfinkelChechikDevereux03] .Close GurfinkelChechikDevereux03 .Open GurfinkelChechikDevereux03 Arie Gurfinkel & Marsha Chechik & Benet Devereux Temporal Logic Query Checking: A Tool for Model exploration IEEE Trans Software Engineering V29n10(Oct 2003)pp898-914 Based on .See [GurfinkelDevereuxChechik02] =IDEA MODAL TEMPORAL LOGIC CTL Placeholders DeMorgan Algebra TLQSolver \chi\_Chek Cruise control SCR CSCI656 Instead of checking a CTL for truth/falsity: compute the formula that "fill in the blanks" in a CTL formula: AG(?1) -- what is always and forever true? AX(?1{p,q}) -- what formula on p and q (only) is always true in the next step? AG(?1 /\ AX?2) -- what pair of formulas ... .Close Guzdial95 .Open Guzdial95 Mark Guzdial<guzdial@cc.gatech.edu> Centralized Mindset: A student Problem with Object-Oriented Programming Papers of the 26th SIGCSE Tech Symposium on CS Ed SIGCSE Bulletin V27n1(Mar 1995)pp182-185 =EDUCATION PEOPLE OBJECT-ORIENTED vs FUNCTIONAL Tendency for students to pack all the logic and structure into a single leader object rather than use communcation and shared responsibillity. Claims result is less reusable. Solutions: Motivate, evaluate alternatives, teach class library, provide experience .Close HaleyLaneyMoffettNuseibeh08 .Open HaleyLaneyMoffettNuseibeh08 Charles B Haley & Robert Laney & Jonathon Moffett & Bashar Nuseibeh Security Requirements engineering: A Framework for Representation and Analysis IEEE Trans Software Engineering V34n1(Jan/Feb 2008)pp133-153 =CASESTUDY SECURITY REQUIREMENTS METHOD Describes a complex process and set of languages that work from security goals, to assets that are to be protected (compare .See [Stoneburner06] ), to requirements, thence to arguments for a particular system design satisfying the requirements, and so to the assumptions that can be rebutted, and the mitigation of the rebuttals and so forth. Security requirements are non-functional requirements and are closely related to the context of the machine being designed. Must expose assumptions about the machine and its context. Arguments that the system satisfies the requirements lead to lists of assumptions that can be challenged (WHY?) and rebutted. Rebuttals lead to mitigators that change the context and/or the requirments. In turn the mitigators can be rebutted, and so on. Hence an iterative process making the design more secure. Uses Jackson Problem Frames ( .See [Jackson95c] .See [Jackson01] ), simplified .See [Toulmin79] arguments, Propositional logic, and a causal logic based on `Event1` shall cause `Event2`. Outer_argument::=`Formal logic showing the design satisfies the requirement and exposing assumptions` Inner_argument::=`Explores assumptions in terms of rebuttals and mitigators`. Process involves engineers and stakeholders in intense and fruitful discussion. (dick)|- Compare .See [Lakatos76] model of the mathematical process. Also methods used to achieve safety. .Close HalleVillemaireCherkoui09 .Open HalleVillemaireCherkoui09 Sylvain Halle & Roger Villemaire & Omar Cherkaoui Specifying and validating data-aware temporal web service properties IEEE Trans Software Engineering V35n5(Sep/Oct 2009)pp669-683 =THEORY TOOL LANGUAGE TEMPORAL LOGIC DATA WEB SERVICES CTL-FO+ PSPACE-complete PROOF .Close HalleVillemaireCherkoui09 .Close HalpernZuck92 .Open HalpernZuck92 Joseph Y Halpern & Lenore D Zuck A Little Knowledge Goes a Long Way: Knowledge-Based Derivations and Correctness Proofs for a Family of Protocols J. ACM V39n3(Jul 1992)pp449-478 .See [CR] (Oct 1993) =THEORY PROVING REFINEMENT PROTOCOLS KNOWLEDGE MODAL LOGIC Argues for the high level design of inefficient solutions that can be shown to be 100% correct and then their refinement into efficient solutions that implement th high level ones. Derives the Alternating Bit Protocol and Stenning's protocol for the Sequence Transmission problem. Defines data flow and how to implement it using unreliable communication. Safety: output sequence is prefix of input sequence. Liveness: all inputs are ultimately output (given fairness). .Close Hamilton01 .Open Hamilton01 Scott Hamilton Formalizing Concept Maps IEEE Computer Magazine V34n1(Jan 2001)pp66+68 (Figure and Side-bar) =IDEA GRAPHIC LOGIC MODEL RKF USER vs FORMAL RKF := Rapid Knowledge Formation. Concept maps are informal concept graphs or semantic nets. .Close HanEtal00a .Open HanEtal00a Yan Ha n & Xu Chun-gen & Zhang Gong-xuan & Liu Feng-yu Constraint specification for object model of access coontrol based on role ACM SIGSOFT Software Engineering notes V25n2(Mar 2000)pp60-64 =PATTERN FORMAL UML LOGIC Dynamic roles form a hierarchy .Close HannaM93 .Open HannaM93 Mary Hanna Reengineering aims for Legacy Salvation IEEE Software Magazine (Sep 1993)p41-48 =POLL ENGINEERING TOOLS REQUIREMENTS .Box MIS Wish List (p41) (all in 4..5 on a 1..6 scale) 1. Capture data defintions 2. Identify problem code 3. Support Version Control 4. Capture Data Models 5. Analyze data flows and logic 6. Capture process model Usage(p42) debug, Test, change management pp44-45+47: Table of 79 vendors selling reeng tools! .Close.Box .Close HansenRavnRischel91 .Open HansenRavnRischel91 Kirsten M Hansen & Anders P Ravn & Hans Rischel Specifying and Verifying Requirements of Real Time Systems ACM SIGSOFT'91 Conf on Software for Critical Systems: Software Eng Notes V16n5(Dec 1991)pp44-54 republished IEEE Trans SE-19n1(Jan 1993)pp41-55 =DEMO TIMING REALITY Requirements SYSTEM LOGIC .Box "1. An application domain system model of the equipment and its intended environment of use is defined. This is a dynamic system model, and defines the overall states of the system as functions of time. Requirements are constraints on this model." 2. control model 3. design model. Interval logic(predicates define durations of states) formal .Close.Box .Close Harel79 .Open Harel79 David Harel First Order Dynamic Logic Springer Verlag 1979 (PhD Thesis MIT 78) =THESIS regular logic structure .Close HarelKozenTiuryn00 .Open HarelKozenTiuryn00 David Harel & Dexter Kozen & Jerzy Tiuryn Dynamic Logic MIT Press 2000 ISBN 0-262-08289-6 $50 QA76.9 L63 H37 =TEXT LOGIC TEMPORAL for cs565/656 .Close Hares90 .Open Hares90 John S Hares SSADM for the Advanced Practitioner John Wiley & Sons NY NY 1990 =TEXT SSADM Content .Box 1 Past and future 2 strengths and weaknesses 3. Pearls of PRactical Wisdom 4 Distributed, Realtime, Conversational 5 Expert Systems & Object Oriented Design .List OOD Normalize logic as well as attributes. access paths ---> responsibillity clusters .Close.Box .Close Hart95 .Open Hart95 Johnson M. Hart Experience with Logical Code Analysis in Software Maintenance Software Practice and Experience V25n11(Nov 1995)pp1243-1262 =DEMO EXPERIENCE PROOF .Box jon@bilbo.radonc.washington.edu, Jon Jacky at University of Washington: The author used simple reasoning about weakest preconditions, postconditions, invariants and logic to find and fix errors in real C code for TCP/IP and other communications software. A nice example of a pragmatic use of formal methods for program derivation and verification. .Close.Box .Close HawkinsEtAl12 .Open HawkinsEtAl12 Peter Hawkins & Martin Rinard & Alex Aiken & Mooly Sagiv & Kathleen Fisher An introduction to data representation synthesis Commun ACM V55n12(Dec 2012)pp91-99 .See http://doi.acm.org/10.1145/2380656.2380677 =TOOL RelC COMPILES RELATIONAL DATA to STRUCTURES HASH LIST VECTOR PERFORMANCE Method:=relational TNF data; logical queries; physical data structures; physical queries; code; performance. Essentially an implementation of Keith Robinson's data design theory from 1980 SSADM! .Close HavelunddLowryPenix01 .Open HavelunddLowryPenix01 Klaus Havelundd & Mike Lowry & John Penix Formal analysis of a Space-Craft Controller using SPIN IEEE Trans Software Engineering V27n8(Aug 2001)pp749-765 =CASESTUDY FORMAL MODEL CHECKING TOOL SPIN LISP LTLMODAL LOGIC ESL PROMELA Deep Space 1. Located a major design flaw. found a bug that testing missed that caused problem 98M kilometers from Earth. LTL::="Linear Temporal Logic", properties of traces using modes [] = always and <> meaning some. Interviewed programmer about impact of work: `found difficult mission-killing bugs -- thought formal meant program proving not finding bugs`. .Close HayAtlee00 .Open HayAtlee00 Jonathan D hay & Joanne M Atlee Composing Features and resolving Interactions .See [FSE8] pp110-119 =CASESTUDY FORMAL EVOLUTION CVF LOGIC Relations POTS A way to add features to a complex system even when they conflict with the system and each other. .Close HayesB05 .Open HayesB05 Brian Hayes Naming Names American Scientist V93 (Jan/Feb 2005) and republished in .See [HayesB08] =ARTICLE CODING DATA .List Internet account IDs NY Stock Exchange Ticker Symbols -- up to 3 Uppercase letters -- 26+26**2+26**3 possible Universal Product Codes -- bar codes -- ( .Key UPC )-- 12-digit until January 2005, and then 13-digits. Global Traded Item Numbers (GTIN) European Article Numbers (EAN) Biological Species -- Two Latin-like words The Chemical Elements -- One uppercase letter + option lower case letter. (I had to program these while working for ICI in the 1960's) Organic Chemicals -- Complex coding. Internet Assigned Number Authority .Key IANA names for countries -- two ASCII letters Radio Call Signs -- 3..4 Capital letters -- KVCR, KFROG, ... Telephone numbers -- 10 digits (in the USA). Social Security Numbers -- 9 digits in the USA Airport codes (IATA) -- Three letters. Names of Horses -- 2..18 characters ( letters plus space, period, and apostrophe). .Close.List .Close Hayes09 .Open Hayes09 Brian Hayes Writing Math on the Web American Scientist V97n2(Mar-Apr 2009)pp98-102 =ARTICLE HTML \TeX TeX MathML JsMath FONTS techexplorer Problems with putting formulae onto web pages. Where to render the formula: author, server, or client? Client: Plugin(techexplorer), fonts, special script (JsMath). Rely on user having the plugins and fonts to work. Server example -- Wikipedia uses `texvc`, MathTeX, MimeTeX. All make graphic images. reliable and ugly. How to render: as a graphical image or using Fonts or Unicode? Failure of MathML to become mainstream. (dick)|-Failure of \TeX to express hypertext markup. (dick)|- No formal syntax and semantics for proofs and logic in \TeX or MathML (dick)|- Still like my $MATHS language better. .Close HazzanDubinsky08 .Open HazzanDubinsky08 Orit Hazzan & Yael Dubinsky Agile Software Engineering Springer Pub NY NY(2008) ISBN 184001983 $CR 0912-1151 =MANUAL PEOPLE AGILE TEAMS TESTS REFLECTION HUMAN ORGANIZATIONAL TECHNOLOGY HOT::analysis=Human >< Organizational><Technological. Describes a process that helps people learn what might be taught directly in other books. Not clear if they are training students or teachers. The treatment of refactoring is completely inadequate. .Close Hehner84a .Open Hehner84a Eric C R Hehner Predicative Programming Part I Commun ACM V27N2 ( Feb 1984)pp134-151 =DEMO dynamic logic regular Next part .See [Hehner84b] .Close Hehner84b .Open Hehner84b Eric C R Hehner Predicative Programming Part II Commun ACM V27n3( Mar 1984) =DEMO dynamic logic regular non-sequential Follows .See [Hehner84a] .Close Heitmeyer02 .Open Heitmeyer02 Constance Heitmeyer Software Cost Reduction Center for High Assurance Computer Systems (CHACS) Publications 2002 .See http://chacs.nrl.navy.mil/publications/CHACS/2002/2002heitmeyer-encse.pdf =HISTORY PARNAS NRL SCR IDEAS NOTATIONS TOOLS TABULAR LOGIC NAT IN OUT REQ A-7E TAME REQUIREMENTS DESIGN MODULES @T(c) ::=`c becomes true`, @F(c)::=`c becomes false`. SCR uses logic and tables to express very clearly what is expected of a new system. Software that monitors certain inputs and controls certain outputs. It uses a four variable model (NAT+REQ+IN+OUT) that distinguishes the assumed properties (NAT) from the requirements (REQ). IN and OUT specify tolerances. Software has `modes`. Tables relate modes and events. Finite State model. Human inspection for defects proved expensive and tools uncovered more defects afterwards. Tools include SPIN, TAME, PVS, Salsa, an invariant generator, . Usable subsets of requirements lead to the `uses hierarchy`, `module guide`, etc.. Methods and tools applied to real projects to discover problems. Also see .See [HeitmeyerEtal98] .See [HeitmeyerKirbyLabaw97] .Close Heitmeyer02a .Open Heitmeyer02a Constance Heitmeyer Software Cost Reduction. Article in .See [Marciniak02] =UNREAD =HISTORY PARNAS NRL SCR IDEAS NOTATIONS TOOLS TABULAR LOGIC NAT IN OUT REQ A-7E TAME REQUIREMENTS DESIGN MODULES Compare .See [Heitmeyer02] perhaps .Hole Heitmeyer02a .Close Hennessy88 .Open Hennessy88 ?? Hennessy Algebraic Theory of Processes MIT Press MA 1988 =TEXT ALGEBRA MATH NONSEQUENTIAL logic .Close HenryFaller95 .Open HenryFaller95 Emmannuel Henry & Benoit Faller Large-scale Industrial Reuse to Reduce Cost and Cycle Time IEEE Software Magazine V12n5(Sep 1995)pp47-53 =EXPERIENCE C++ TECHNICAL REUSE COST PROCESS .Box Note sizes 400...500KLOC of C++ EXPERIENCE Separated physical, GUI, Data comms, data base and logic of a naval permanent system and could then reuse the physical,GUI.... parts in an mobile army system significant speed up in delivery, productivity and 30% decraes in the number of faults/LOC. Also used incremental delivery to validate and improve GUI. Claims that there is much to be said for starting out with reusing what you have on the way to developing a new process. Use of good design, and C++. Design elements are about 20 classes. functional set(subsystem has 30..100 design elements). Reuse 20..50%, faults down 15%..50% as well. .Close.Box .Close HermenegildoEtAl08 .Open HermenegildoEtAl08 M V Hermenegildo & F Bueno & N Carro & P Lopez & J F Morales & G Puebla An Overview of the Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy Montanari Festschrift pp208-237 .See [DeganoEtAl08] =ADVERT LANGUAGE Ciao TOOL THEORY FUNCTIONAL OO LOGIC CONSTRAINT Downloads .See http://www.ciaohome.org .See http://www.cliplab.org .See mailto:ciao@clip.dia.fi.upm.es 91 references .Close Hersh95 .Open Hersh95 Ruben Hersh Fresh Breezes in the philosophy of Mathematics American Math Monthly V102n7(aug-sep 1995)pp589-594 =HISTORY MATHEMATICAL LOGIC .Box logicism, formalism, intuitionism have produced no solutions to the question of why math works as well as it does. Compares history to the philosophy of science: Phil/Sc went thru a logical positivist phase of (axioms, maps, theories) before people studied what real scientists do... Humanistic ideas about math: human, fallible, rigor varies, empirical clues and numerical experiments and probabilities help more than logic, objects as social-cultural-historical objects p593: "Study of the lawful, predictable parts of the physical world has a name. That name is 'physics'. Study of the lawful, predictable parts of the social-conceptual world has a name. The name is 'mathematics'." .Close.Box Compare .See [Lakatos76]. .Close HincheyEtAl08 .Open HincheyEtAl08 MIke Hinchey & Michael A Jackson & Patrick Cousot & Byron Cook & Jonathen P Bowen & Tiziana Software Engineering and Formal Methods Commun ACM V51n9(Sep 2008)pp54-59 .See http://doi.acm.org/10.1145/1378727.1378742 $CR 0908-0760 =SURVEY FORMAL MATHEMATICAL LOGICAL METHODS TOOLS QUALITIES RELIABLE COST Summary of three key note speeches from ICSE&FM 2007. Describes history: increasing dependability of hardware, more intensive use of software, more ubiquitous computing, no increase in software dependability. Formal methods can increase dependability. Jackson notes that good engineering stays within the .Key normal design discipline associated with a given application domain. .Key Radical design leaves the normal and always decreases the dependability of the result. Therefore the need to develop special purpose disciplines for each domain. Refers to .See [Vincenti90] on engineering. Compare with Henry Petrosky's work. Patrick Cousot defines formal methods and the idea of abstraction. Mentions Astree. Byron Cook notes the explosion of complexity when there is concurrency and the attempts to overcome it. Conclusion reviews the history, describes .Key method engineering and states that the quest continues... .Close Hoare69 .Open Hoare69 C.A.R. Hoare An Axiomatic Basis for Computer Programming Commun ACM V12 n10 Oct 69 =THEORY logic formal structures .Close Hoare78 .Open Hoare78 C.A.R. Hoare Communicating Sequential Processes Commun ACM v21 n8 pp666-677(Also book -See .See [Hoare85] ) =THEORY non-sequential logic CSP Contrast .See [Milner80] CCS .See [Baetan90] ACP .Close Hoare85 .Open Hoare85 C.A.R. Hoare Communicating Sequential Processes Prentice Hall 1985 =IDEA CSP non-sequential formal logic structures Developed from .See [Hoare78] Contrast .See [Milner80] .See [Baetan90] ACP Later edition(2006) online .See http://www.usingcsp.com/cspbook.pdf as PDF. .Close Hoare09 .Open Hoare09 C A Hoare retrospective: an axiomatic basis for computer programming Commun ACM V52n10(Oct 2009)pp30-32 .See http://doi.acm.org/10.1145/1562764.1562779 =HISTORY VERIFICATION PROGRAMMING LOGIC PROOFS TESTS HACKERS SPECIFICATIONS COSTS Looking back at .See [Hoare69] 40 years later. Compare .See [Hoare01] Expected to retire before research was complete and industry adopted methods. Surprised to find "assert" in C/C++. Didn't expect the new logics/mathematics that have been developed. Tests test the programmer not the program. Hackers have got industry interested in verification -- finally. Academic and industrial research should complement each other. One goes for the big ideals and the other for low hanging fruit. Reply .See Humelsine10 (letter). .Close Hoareetal87 .Open Hoareetal87 C.A.R. Hoare & IJ Hayes & HE Jifeng & CC Morgan &AW Roscoe & JW Sanders & IH Sorenson & JM Spivey & BA Sufrin Laws of Programming Commun ACM V30n8 (pp672-686)1987 =IDEA formal sequential logic For practicing engineers mathematical laws are also more relevant than the elaborate models constructed in a study of foundations. could define programs as relations that are total and with images that are either finite or else universal with fictitious "state at infinity" for non-termination. finite texts have a normal form ignoring speed. .Close HoareBroySteinbruggen01 .Open HoareBroySteinbruggen01 Tony Hoare & Manfred Broy & Ralf Steinbruggen Engineering theories of Software Construction IOS Press(2001) Amsterdam, The Netherlands ISBN 1586031724 CR 0304-0310 =WORKSHOP ENGINEERING MATH LOGIC MODELING PROBLEM-FRAMES REALITY REACTIVE Petri .Close Hodges77 .Open Hodges77 Wilfrid Hodges Logic Penguin Books Middlesex UK & NY NY 1977 =TEXT FORMAL LOGIC Semantic Tableaux TREEs Describes an easy to learn and use method of proving/disproving results. Compare with earlier .See [Jeffrey67] and next edition .See [Hodeges05] .Close Hodges05 .Open Hodges05 Wilfred Hodges An Introduction to Elementary Logic, Second Edition $20.00 Paperback | 5.07 x 7.79in | 304 pages | ISBN 9780141003146 | 28 Dec 2005 | Penguin UK =TEXT FORMAL LOGIC Semantic Tableaux TREEs Describes an easy to learn and use method of proving/disproving results. Based on earlier .See [Jeffrey67] .Close Hoffman08b .Open Hoffman08b Leah Hoffman Talking Model-checking Technology =INTERVIEW HISTORY MODEL CHECKING VERIFICATION FSM TEMPORAL LOGIC Commun ACM V51n7(Jul 2008)pp112+110-111 Interview with Turing prize winners E Allen Emerson & Edmund M Clark & Joseph Sifakis Painful birth: theoretically trivial and practically impossible! Handle programs that do not stop. Avoid humans proving programs. Based on finite state abstractions of program+hardware and requirements specified in temporal logic. If property is not satisfied by abstraction then procedure gives a diagnostic trace of the bad behavior. Problem: State Explosion: no of cases to consider can grow exponentially with the size of the model. Benefits: precise specifications. Limits: 10^100 states! Microsoft has one used for device drivers! .Close HoffmanWeiss01 .Open HoffmanWeiss01 Daniel M Hoffman & David M Weiss Software fundamentals: Collected Papers by David L Parnas Addison-Wesley 2001 CR0109-0914 ISBN 0-201-70369-6 QA76.754P36 =COLLECTION REQUIREMENTS MODULES DESIGN LOGIC TECHNICAL SCR TABULAR LANGUAGES METHODS SDI A7 ENGINEERING .Close Holloway95 .Open Holloway95 C Michael Hollowy<c.m.holloway@larc.nasa.gov> Software Engineering epistomology ACM SIGSOFT Software Engineering Notes V20n2(Apr 1995)pp20-21 =SURVEY LOGIC FALACIES PROCESS IMPROVEMENT How do we know that something is true: .Box Authority Divine -> Absolute truth Human -> Opinion Reason Logic -> Conditional Absolute Truth Experience Anedotal Experience -> Possible truth Experimental Experience -> Probable truth Pronouncements with little logic or experiemne. Resistance to data collection in projects .... .Close.Box .Close HollowayButler96 .Open HollowayButler96 C Michael Hollowy<c.m.holloway@larc.nasa.gov> & Ricky W Butler Impediments to Industrial Use of Formal Methods IEEE Computer Magazine V29N4(Apr 1996)pp25-26 =EXPERIENCE FORMAL METHODS .Box NASA Langley Research center spnsoring industrial projects: AAMP-FV processor, toold manipulating decision tables. showed impediments: tools, examples, expectations that tools sell themselves. Tools: "Not only do the input languages use specialized notations from mathematical logic, but many tools have numerous bugs in them. Few things are more disconcerting..." need to improve quality of current not their power. Examples are toy, interesting but irrelevnt The first effort in a new domain requires far greater creativity than subsequent efforts. need to provide guidance for executives on matching method to applications. unbiased assessments. .Close.Box .Close Holzmann02 .Open Holzmann02 Gerard J. Holzmann The Logic of Bugs SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp81-87 online at .See http://doi.acm.org/10.1145/587051.587064 =Keynote BUGS V&V SQA MODEL CHECKING TOOLS NOTATIONS LOGIC GRAPHIC LTL SPIN TimeLineEditor Human fallibility: abut 12 errors in 13800 sentences in a typical NYTimes. Careful programmers have similar error rates(?). Argues that bugs evolve: the mutate and only some type survive. The weakest point is where the bugs are to be found. The weak point in model checking is the language used to specify requirements. Suggests using a graphic notation instead of a temporal logic. .Close Honidenetal94 .Open Honidenetal94 Shinichi Honiden & Kazuhiko Nishimura & Naoshi Uchihira & Kiyoshi Itoh An Application of Artificial Intelligence to Object-Oriented Performance Design (OOPD) for Real-Time Systems IEEE Trans SE VSE-20n11(Nov 1994)pp849-867 =DEMO LOGIC NONDECLARATIVE OBJECT-ORIENTED PROLOG MENDEL Automatic redesign of lift controler to avoid bottleneck .Close Horrocks08 .Open Horrocks08 Ian Horrocks Ontologies and the Semantic Web Commun ACM V51n12(Dec 2008)pp58-67 .See http://doi.acm.org/10.1145/1490360.1409377 =POPULARIZATION WEB ONTOLOGIES SEMANTICS LOGIC RULES RDF OWL Figure 2:the .Key Tree of Porphyry .See http://en.wikipedia.org/wiki/Tree_of_Porphyry (Wikipedia) and .See ./maths/http://csci.csusb.edu/dick/maths/logic_8_Natural_Language.html#Stuff (MATHS) RDF expresses labelled directed graphs: subject --(verb)--> Object. What we used to call semantic nets in the 1970s. .Close HouHoover06 .Open HouHoover06 Danqing Hou & H James Hoover Using SCL to Specify and check Design Intent in Source Code IEEE Trans Software Engineering V32n6(Jun 2006)pp404-423 =CASESTUDY TOOL V&V SQA STATIC CHECK TECHNICAL CODE Java C++ MVC SCL::="Logic based language and tool that expresses and checks constraints on object-oriented code" Typical constraint: In Java all classes derived from Object should define a `public boolean equals(Object o) method`, not one with another parameter type. Lint for the 21st century. .Close Humby73 .Open Humby73 E Humby Programs from Desion Tables Macdonald London UK & American Elsevier NY NY 1973 ISBN 0-356-04126-3 & 0-444-195969-6 respectively LCCard#72-90803 =HANDBOOK Tables SQA REQUIREMENTS QUALITY COMPLETENESS AMBIGUITY implementation COBOL A .Key Decision Table is an early non-procedural and non-language description of requirements and logic. They can be translated into code. Manually they where difficult to maintain. They are a table with two parts. First come the conditions -- one per row and then come the actions. Each condition can (in a simple decision table) have one of two values: T or F. The columns indicate T, F, and - (either). In the actions an X indicates an action to be done and a - one that is not done (we can also use A,B,C, ... in a column to indicate the sequence of actions. Example Decision table from page 88 .Table Labels Rules 1 2 3 4 .Row C1 He knows N N Y Y .Row C2 He knows C1 N Y N Y .Row A1 Shun him X - - - .Row A2 Teach him - X - - .Row A3 Wake him - - X - .Row A4 Follow him - - - X .Close.Table .Close Humphrey95a .Open Humphrey95a Watts S Humphrey (SEI) A Discipline for Software Engineering Addison-Wesley Redwood City CA 1995 (SEI Series in software Engineering) ISBN 0-201-54610-8 BNB 93-41673 QA76.758H857 =TEXT PSP IMPROVEMENT ESTIMATION METRICS .Box PSP=Personal Software Process (ac)|- Did not work well as CS455(Software Engineering) text. Includes logic and statistics! Goal-Question-Metric. Tables("Templates") in chapter 10 "software design". See .See [Humphrey95b] for quick summary. Reviewed by Tom DeMarco: revolutionary idea that individuals should be responsible for estimation and measurement, not institutions. Weakest in low-level design. IEEE Computing Magazine Oct 1995 pp82-83 Follow ups: Textbook on PSP: .See [Humphrey97;] the Team Software Process( .See [TSP] ), introduction .See [Humphrey00] .Close.Box .Close HuntbachRingwood95 .Open HuntbachRingwood95 Mathew M Huntbach & Graem A Ringwood Programming in Concurrent Logic Languages IEEE Software Magazine(Nov 1995)pp71-82 =PAPER TECHNICAL NONSEQUENTIAL vs NONDETERMINISM BACKTRACKING PERFORMANCE adding paralelism efficiently means redefining nondeterminism and so abandoning backtracking with result that is not logic programming .Close HunterNuseibeh97 .Open HunterNuseibeh97 Anthony Hunter & Bashar Nuseibeh Analysing Inconsistent Specifications .See [RE'97] pp78-86 =FORMAL REQUIREMENTS LOGIC REQUIREMENTS LOGIC must not include `ex falso quodlibet` and should track all inferences from stated requirements to conclusions and so aid diagnosis of inconsistencies QC::="Quasi Classical Logic" .Close HunterNuseibeh99 .Open HunterNuseibeh99 Anthony Hunter & Bashar Nuseibeh Managing Inconsistent specifications: Reasoning, Analysis, and Action ACM ToSEM V7n4(May 1999)pp335-367 =IDEA labelled QC Quine FORMAL LOGIC SPECIFICATION Label requirements and record deductions so that you can back track when inconsistent ones emerge. .See [QC] Compare with the way mathematicians handle inconsistencies in .See [Lakatos76]. (dick)|- my MATHS notation uses .As_is (reason, reason, ...)|-(label): statement. to record such connections but does not allow the same freedom in abandonning and adjusting the logic. .Close HuthRyan00 .Open HuthRyan00 Michael R Huth & Mark Ryan Logic in Computer Science: Modeling and reasoning about systems Cambridge U P 2000 ISBN 0 521 65200 6 (hardback) ISBN 0 521 65200 8 (paperback) =TEXT FORMAL MODEL LPC MODAL LOGIC CTL OBDDs AGENTS VERIFICATION SMV CSUSB.CSCI556/656 .Close JacksonD00 .Open JacksonD00 Daniel Jackson Automating first-Order Relational Logic .See [FSE8] pp120-139 =THEORY LOGIC RELATIONS PREDICATE Z OCL =DEMO TOOL 50KLOC Java SAT Alloy Analyzer Nitpick UML COM Mobile IP Shorter than SMV by 10 times. Quantifiers make logic easier to use. Analysis s faster than Nitpick as well. Describes syntax, type rules and semantics of the logic. In place of composition of relations ( R; S = rel[x,z](some y, x R y S z)), defines navigation ( R . S = rel[x,z](some y, y R z and y S x)) scalar variables are replaced by singleton set variables. analysis:= normalize and skolemize; boolean formula; conjunctive normal form; SAT solver; map back to relational. Alloy_Analyzer::=http://sdg.lcs.mit.edu/alloy Proved UML meta-model is consistent in less than 20 seconds. See also .See [JacksonDSullivan00] .Close JacksonD02 .Open JacksonD02 Daniel Jackson Alloy: A Lightweight Object Modeling Notation ACM TOSEM Trans Software Eng & Methodology V11n2(Apr 2002)pp256-290 =IDEA GRAPHIC FORMAL Object-Oriented NOTATION Alloy Z SEMANTICS LOGIC SETS RELATIONS FUNCTIONS .Close JacksonD06a .Open JacksonD06a Daniel Jackson Software Abstractions: Logic, Language, and Analysis The MIT Press Cambridge MA 2006 ISBN 0262101149 $CR 0802-0116 0806-0536 , rev edn 2012 ISBN 0262017156 $CR 1211-1092 1212-1193 =TEXT Alloy LIGHT FORMAL MODEL CHECKING METHODS TOOLS A neat way of finding bugs in specifications and requirements. Small_scope_hypothesis::=`Most bugs have small counterexamples`. Notes the difficulty of creating consistent formal models that have the desired properties. Alloy::language=`a formal first order relational logic expressed in ASCII with tools in Java`. Alloy_examples::=http://softwareabstractions.org. Alloy_analyzer::=http://alloy.mit.edu. .Close JacksonDShlyakhterSridharan01 .Open JacksonDShlyakhterSridharan01 Daniel Jackson & Ilya Shlyakhter & Manu Sridharan A Micromodularity Mechanism ACM SIGSOFT proc ESEC-8 FSE-9 Software Engineering Notes V26n5(Sep 2001)pp62-73 =IDEA MODULAR SPECIFICATIONS RELATIONS FORMAL NOTATION LOGIC EXTENSION TOOL? cf Z Alloy On the WWW .See http://sdg.lcs.mit.edu/~dnj/publications |- A structure is a set of atoms and its fields are global relations that map atoms to other sets of atoms. |- Structure extensions are just subsets. sig name [parameters] extends parent[parameters]{ field: associate ...}{properties}: field is a relation between name and associate and name is a subset of parent. fact { property }: makes assumptions, states constraints, can retrofit fields assert{properties}: theorems -- properties that are intended to hold, and so need checking. fun name(para:type...){property}: defines properties that may or may not be true. used to describe methods, abstraction. Simpler and more focused than Z, VDM, or MATHS .Close JacksonVaziri00 .Open JacksonVaziri00 Daniel Jackson & Mandana Vaziri Finding Bugs with a Constraint Solver Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp14-25 =DEMO LOGIC Alloy disproving find scope limited models of (Pre and Code and nou Post ) Programs with pointers often have errors exposed in seconds. Worst 6 minutes. .Close Jacquet93 .Open Jacquet93 Jean-Marie Jacquet Constructing Logic Programs John Wiley & Sons NY NY 1993 ISBN 0-471-93789-4 CR9601-0007(D.1.6) skeletons + links to OO .Close JaspanEtAl09 .Open JaspanEtAl09 Ciera Jaspan & Michael Keeling & Larry Maccherone & Gabriel L. Zenarosa & Mary Shaw Software mythbusters explore formal methods IEEE Software Magazine V26n6(Nov/Dec 2009)pp60-63 =REPORT DISCUSSION EXPERIENCE MYTHS FORMAL METHODS AGILE FSM LOGIC MATHEMATICS Reference a list .See [Hall90] of seven myths Formal methods are richer than in 1990. They are now used in requirements to get precision and understanding. They are embedded in tools and environments reducing the need for mathematical maturity. They enable communication and evolution and so support agility. An FSM model for understanding lead to better code. Must match the method to the problem cost-effectively. Formal methods are being domesticated. .Close Jeffrey67 .Open Jeffrey67 Richard C Jeffrey Formal Logic: Its Scope and Limits McGraw-Hill NY NY 1967 =TEXT FORMAL LOGIC semantic Tableaus TREES An easy to use way of proving things. Compare with the later .See [Hodges77] and .See [Jeffrey91] .Close Jeffrey91 .Open Jeffrey91 Richard C Jeffrey (Princeton U) Formal Logic: Its Scope and Limits McGraw-Hill Higher Education NY NY 1991 ISBN 0-07-032357-7 =TEXT FORMAL LOGIC semantic Tableaus TREES An easy to use way of proving things. Improved edition of .See [Jeffrey67]. Compare with the earlier .See [Hodges77] .Close JonesCB95 .Open JonesCB95 Cliff B Jones Partial Functions and Logics: A Warning IPL V54n2(??? 1995)pp65-67 =THEORY FORMAL LOGIC See .See [LPT] and .See [LPV] .Close JonesJones91 .Open JonesJones91 Peter C Jones & Paul E Jones Jr Data Theory Prentice Hall Int Englewood Cliffs NJ 1991 QA76.9.D3 CR9206-0367 =theory logic incomprehensible .Close JuristoMorenoLopez00 .Open JuristoMorenoLopez00 Natalia Juristo & Ana Maria Moreno & Marta Lopez How to Use Linguistic Instruments for Object-Oriented Analysis IEEE Software Magazine V17n3(May/Jun 2000)pp80-89 =DEMO METHOD OOA/D LANGUAGES BNF OMT step by step way to map requirements via objectmodel (OM) plus behavior model (BM) to OO? design Starts with informal requirements, but notes errors occur in them. Splits into static vs dynamic. Translates into 1:special language; 2: OMT+martin missing(p85) : using normalization to assign attributes to class. missing(pp88-89) :ref to NIAM? wrong(p87) : when a method operates on all the classes in a sub-hierarchy "the method will belong to the highest class". leads to anomolous classes with no behaviors plus highlevel classes with complex logic and so reduced maintainabillty. .See [BottingJuristo00] .Close Kahn92 .Open Kahn92 Ken Kahn A Braid of Research Threads(in The Fifth Generation Project) Comm ACM V36n3(Mar 1993)pp77-82 =EXPERIENCE OBJECT-ORIENTED GRAPHIC DESIGN .Box p79-80 "Saraswat and I began work on a visual syntax for concurrent logic programs. he Syntax was based on the topology of drawings. It was designed so that it was well suited not just for program sources but also as a basis for generating animations of program executions. One discovery was that object-oriented programs did not come out so clumsy and verbose when they where drawn instead of typed. " .Close.Box .Close KalishMontague64 .Open KalishMontague64 Donald Kalish & Richard Montague Logic: Techniques of formal reasoning Harcourt Brace & World Inc. NY NY 1964 =TEXT LOGIC Natural deduction with boxes withn boxes. Brilliant. .Close Katz90 .Open Katz90 Robert L Katz Business/Enterprise Modeling IBM Systems Journal V29n4(1990)pp509-525 =ADVERT MODEL DATA PROCESS .Box p510..511(Figures 1 &2) modeling across the life cycle(data,process, network)><scope, ERD,Logical, technology=design, detailed=implemented) .Close.Box .Close KauffmannMoore97 .Open KauffmannMoore97 Matt Kaufmann & J S Moore An Industrial Strength Theorem Prover for a Logic Based on Common LISP IEEE Trans Softw Eng VSE23n4(Apr 1997)pp204-213 .See http://www.cli.com/ =EXPERIENCES PROOF LOGIC LISP ACL2 hardware CLI Nqthm .Close Kaye07 .Open Kaye07 Richard W Kay The Mathematics of logic: a guide to completeness theorems and the applications Cambridge UP NY NY 2007 ISBN 052170877X $CR 0902-0126 =UNREAD THEORY LOGIC MATHEMATICS SEMANTICS Zorn AC Posets TARSKI P=NP .Close KazmanChen90 .Open KazmanChen90 Rick Kazman & Hong-Mei Chen the metropolis model -- a new logic for development of crowdsourced systems Commun ACM V52n7(Jul 2009)pp76-84 .See http://doi.acm.org/10.1145/1538788.1538808 =ESSAY WEB/NET COMMONS F/OSS ONION SERVICES CROWDSOURCE JAD CBSS LIFECYCLE ANALYST DESIGN ECONOMICS ITERATION. DISTRIBUTED EVOLUTION PEOPLE COMMONS CBSS::="community-based service systems", following .Net not producing goods for consumption. Not centralized. open teams. Mashability -- reuse. conflicting, unknowable requirements -- discover by doing, emergent. Continuous evolution. Focus on operations. Start with a working system and aim for no downtime. Sufficient correctness. Perpetual Beta. Unstable resources -- many parallel prosumers. prosumer::= produce & consumer. Emergent behavior. Nondeterministic. .Close.Net metropolis_model::onion=kernel+periphery+masses. principles: .Box crowd management>project management. promotion through ranks, attracting developers, meritocracy. split kernel services from peripheral services. pernipheral work is done by crowdsourcing, kernel by higher ranked developers. ubiquitous operations even as it evolves. .Close.Box implications: no phases, align business to crowd, not control but lead, tutorials and examples, usability. Requirements come from the periphery, forums help but can be shortcircuited. Architecture vital core. Small modular kernel. Tools for Testing, bug reporting and tracking. Flexible delivery. High availability. .Close KennedyEberhart02 .Open KennedyEberhart02 James Kennedy & Russell C Eberhart Swarm Intelligence Morgan Kaufman 2001 ISBN 1-55860-595-5 QA337.3 K45 =IDEA NON-ALGORITHMIC NONSEQUENTIAL OPTIMIZATION In a swarm individuals tend to both move toward their topological neighbors, but also toward the individual that seems to be doing best. Claims to be useful and effective. Overgeneralized (?) to argue that intelligence is dependant on the interaction of individuals. Useful survey of many years of experiments with systems made of interacting individuals. .Close Khanna91 .Open Khanna91 S Khanna Logic Programming for Software Verification and testing Comput Jnl V34n4(Aug 1991)pp350-357. =DEMO LOGIC V&V TESTING .Close Kiniry02 .Open Kiniry02 Joseph R. Kiniry <kiniry@acm.org> Semantic Component Composition Submitted to GCSE/SAIG '02, arXiv.org e-Print archive Mon, 15 Apr 2002 .See http://www.arxiv.org/abs/cs.SE/0204036and Ph.D. Thesis CalTech. =ADVERT THEORY MODULES CORRECTNESS CONTRACT REUSE COMPONENTS SEMANTICS Kind-theory LOGIC QUALITIES BON Jiki author attempted to develop a way to describe components, calculate inter-operation, and to lead automatically generating adapters to connect components. `instance : kind` kinds: 2 inheritance relations, 2 inclusion relations, several equivalences, 2 realization relations, 3 composition operators, 2 interpreter mappings, a canonical operator [_] Compare with many previous logistic systems going back to Aristotle. semantic_ properties:=meta_information | dependencies | inheritance | contractual | concurrency | usage | pending_work | versioning | documentation | Miscellaneous. meta_information:= author | bon | bug | copyright | description | history | license | title, dependencies:= references | use. inheritance:= hides | overrides | realizes, contractual:=ensure | generate | invariant | modifies | require, usage:= param | return | exception. pending_work:= idea | review | todo. versioning:= version | deprecated | since. documentation:= design | equivalent | example | see. Miscellaneous:= guard | values | time_complexity | space_complexity. .Close Kleinberg08 .Open Kleinberg08 Jon Kleinberg The Convergence of Social and Technological networks Commun ACM V51n11(Nov 2008)pp66-72 .See http://doi.acm.org/10.1145/1400214.1400232 =EMPIRICAL 6DEGREES SMALL WORLDS GRAPHS WEB/NET Milgram SOCIOLOGY CONTAGION MIMETICS IDEAS Evidence that real social networks are "small worlds" as predicted. Evidence that ideas spread in jagged trees through the network. "Contagion as a Design Priciple" .Close KoMyersCoblenzAung06 .Open KoMyersCoblenzAung06 Andrew J Ko & Brad Myers & Micheal J Coblenz & Htet Htet Aung An Exploratory Study of How Developers Seek, Relate, and Collect Relevant Information during Software Maintenance Tasks ICSE'05 & IEEE Computer Magazine V39n12(Dec 2006)pp971-987 =EXPERIMENT SIMULATED MAINTENANCE INTERUPTIONS TECHNICAL Eclipse Java Swing Paint Information_Foraging::=the BIBLIOGRAPHY(authors=>"P Pirolli &S K Card", title=>"Information Foraging", citation=>"Psychological Review V106n4 (1999)pp643-675"). Took video records of developers modifying and correcting bugs in apaint program. Coded the actions into 9 types: Handling information(15%), reading code(12%), editing code, navigating dependencies, searching for names, testing, reading Java API, switching applications,reading task description(2%). Early perceptions of bugs can lead to wasted time exploring irrelevant code. Enhancements: developers had to search for a place to extend the existing framework and for examples to copy and modify. Developers used "Find" dialog, Eclipse's multiple windows, What is relevant? When interupted developers always complete there current editting task before acknowledging the interuption, but sometimes forgot to save the edited file! Three states: Search; Relate; Collect. Need better ways to search for relevant code. Good names are vital! Perhaps use hovering to show header info on methods fro example. Need less overhead in navigating and viewing code. EG highlight code to show dependencies of nearby code rather than menus. Show many fragments of code in separate subwindows? See .See [KoMyers10] .Close Kobryn02 .Open Kobryn02 Chris Kobryn Will UML 2.0 Be Agile or Awkward Commun ACM V45n1(Jan 2002)pp107-110 =HISTORY UML 1.* =ESSAY on UML 2.0 Second system effect: .See [Brooks95] UML2.0 will have 4 parts: infrastructure, superstructure, OCL, and Diagram Interchange Resources .See http://www.omg.org/uml .See http://www.uml-forum.com/ .See http://www.telelogic.com/publications/uml_models/ .Close Kowalski79 .Open Kowalski79 Robert Kowalski Algorithm=Logic+Control Commun ACM V22n7(Jul 1979)pp424-436 =DEMO logic-programming non-sequential prolog optimization .Close Kowalski79b .Open Kowalski79b Robert Kowalski Logic for Problem solving Elsevier Science NY NY 1979 1983 ISBN 0-444-00365-7 QA76.K68 =TEXT LOGIC FORMAL PROLOG THINKING .Close Krakovsky11 .Open Krakovsky11 Marina Krakovsky Deus Ex Machina Commun ACM V54n5(May 2011)p22 .See http://doi.acm.org/10.1145/1941487.1941496 =ARTICLE PROOF ONTOLOGICAL EXISTENCE GOD PROVER9 LOGIC PROVER9 Authors Paul Oppenheimer and Edward Zalta: "A Computationally-Discovered Simplification of the Ontological Argument". Australasian Journal of Philosophy 89 (2): 333-349. 2011. Details .See http://mally.stanford.edu/cm/ontological-argument/ More at .See http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.151.7483&rep=rep&type=pdf (PDF). .Close KrishnamurthiFisler07 .Open KrishnamurthiFisler07 Shriram Krishnamurthi & Kathi Fisler Foundations of Incremental Aspect model-checking ACM TOSEM Trans Software Eng & Methodology V16n2(Apr 2007)pp1-39 =THEORY ASPECT MODULES EVOLUTION FSM CTL MODAL LOGIC Models code as finite state machines with special (paired) transitions for entering and leaving subprograms. Aspects are modeled as finite state machines that are place in before/after/arround the special transitions. Aspects placed using regular expression on the state of the stack of calls. CTL modal operators used to state required properties. .Close Krug00 .Open Krug00 Steve Krug Don't Make me Think: A Common sense approach to web usability New Riders 2000 TK5105.888 K78 ISBN 0-7897-2310-7 =GUIDE USER HCI WWW/NET PEOPLE TEAMS "Advanced Common Sense" `Expert usability review` != `usability testing` (1) self evident | (2) self explanatory Users scan pages, they don't read them. We guess. We muddle through. Visual hierarchy and logic. Conventions. Break up into areas. Make clickabilty obvious. Minimize noise. Omit words! Instructions and happy talk. ask(search) or browse? navigation info: site id, utilities( a way home, a way to search,...), contents(with drop down secondary navigation) Page names on all pages, and match link text that refs them. bread crumbs: You are here X>Y>Z>... Tab dividers. Drawn right and front tab clearly in front. home pages: all the above + tag line + ...+where to start design team problems: wars of religion -> resolve by testing the particular case How to do usability tests..... .Close Kruchten95 .Open Kruchten95 Phillipe B Kruchten(Rational Software pjruchten@rational.com) The 4+1 View Model of Architecture IEEE Software Magazine(Nov 1995)pp42-50 =ADVERT SCENARIOS METHOD logical+process+physical+development centered on Scenarios each view uses Elements+forms+rationale/constraints .Close Kruchten08 .Open Kruchten08 Philipe Kruchten The Biological Half-life of Software Engineering Ideas IEEE Software Magazine V25n5(Sep/Oct 2008)pp10-11 =SURVEY IDEAS 1988..2008 Half_life(C)::=`The time taken before 50% of a chemical C is removed from a body`, example: Half_life(caffeine) =~= 3.5.hrs. Out of 50 items in IEEE Software from 1988 no more than 3 are still important. This implies a Half_life of about 5.years. Professional organizations enforce continuing professional development. More important to learn how to learn than learn the language/system of the day. (dick)|- Compare the half life used to model radioactive decay. (dick)|- Suggests exponential decay: amount (t) = amount (t0) * 2 ** ((t0-t)/ half_life) ). (dick)|- `Which ideas are strong enough to survive?` .Close Kung89 .Open Kung89 C H Kung Conceptual Modeling in the Context of Software Development IEEE Trans Soft Eng vSE-15 n10(Oct 1989)pp1176-1187 =DEMO data ERD DFDs logic Petrie nets System .Close KuperVardi93 .Open KuperVardi93 Gabriel M Kuper & Moshe Y Vardi The Logical Data Model (LDM) ACM Trans Database Syst v18n3(Sep 1993)pp379-413 CR9407-0472 =THEORY DATA theory for LDM OO data model that generalizes the relational hierarchical and network review of 7 other attempts none provide both conceptual data and a well defined retrieval mechanism/query language defines a DB schema as a digraph. leaves are dta, internal nodes are connections from objects with separate names and values. sect 2 intro, sectn 3 math defs, sectn 4 logic og LDM, sectn 5 & 6 query languages Strong theoretical foundation for future DBMSs .Close Kurki-Suonio94 .Open Kurki-Suonio94 Reino Kurki-Suonio<rks@cs.tut.fi> Real-Time: Further Misconceptions (or Half-Truths) IEEE Computer Magazine V27n6(Jun 1994)pp71-76 =ESSAY REAL TIME .Box confusion of theoretical model with coded programs.. problems defining real-time systems... possibility of fairness allowing the logical specification of deadlines. .Close.Box .Close KwonAgha11 .Open KwonAgha11 YoungMin Kwon & Gul Agha Verifying the evolution of probability distributions governed by a DTMC IEEE Trans Software Engineering V37n1(Jan/Fed 2011)pp126-141 =THEORY DEMO TOOL MODAL LOGIC MODEL CHECKING iLTL MARKOV DISCRETE TIME BUCHI Model has both probabilities and qualities on transitions and so expected value on paths. Probabillitues and qualities used to give modes in the logic. .Close LafontaneLedruSchobbens91 .Open LafontaneLedruSchobbens91 Christine Lafontane & Yves Ledru & Pierre-Yves Schobbens An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM case Study Commun ACM V45n5(May 1991)pp62-ff =EXPERIMENT FORMAL VDM LOGIC Review: CR 9204-0229 .Close Lakatos76 .Open Lakatos76 Imre Lakatos (edited by John Worral and Elie Zahar) Proofs and Refutations Cambridge University Press 1976 =PHILOSOPHY MATHEMATICS PROOFS SOCIAL PROCESS Describes an advanced seminar in mathematics where the students duplicate the key points in the history of a particularly elegant theorem in the theory of polyhedra. He makes it clear that proofs are often refuted. Mathematics grows by a process of proof, refutation, and reproof. The exception improves the rule more often than not. The author wanted to decrease the dogmatism of mathematics, and in particular the dogma that mathematical knowledge grows by deducing truth from known truths. He shows that actual mathematics develops in an illogical fashion because it grows by discovering the underlying assumptions as well as by working from these to prove conclusions. The end result of years of exploration is an axiomatic structure like Euclid. But this structure is not how the field developed. Lakatos tabulates specific ways of tackling facts that don't fit the theorem and its (putative) proof. See .See [DeMilloLiptonPerlis79] .Close Lamport90a .Open Lamport90a Leslie Lamport A Temporal Logic of Actions(TLA) Report 57 from Systems Research Center Digital Equipment Corpn(1st Apr 1990) & Revised as Lamport91 =MATHEMATICAL non-sequential formal dynamic modal logic .Close Lamport91 .Open Lamport91 Leslie Lamport The Temporal Logic of Actions(TLA) Report 79 from Systems Research Center Digital Equipment Corpn(25th Dec 1991) =MATHEMATICAL non-sequential formal dynamic modal logic Revision of Lamport90b .Close Lamport94a .Open Lamport94a Leslie Lamport Processes are in the Eye of the Beholder Report #132 from Systems Research Center Digital Equipment Corpn(25th Dec 1994) =THEORY NONSEQUENTIAL LOGIC .Box (abstract) A two-process algorithm is shown to be equivalent to an N-process one, illustrating the insubstantiality of processes. A completely formal equivalence proof in TLA (the Temporal Logic of Actions) is sketched. .See http://www.research.digital.com/SRC/publications/src-rr.html .Close.Box .Close Lamport94b .Open Lamport94b Leslie Lamport Unknown ACM TOPLAS (May 1994)pp872-923 =MATHEMATICAL non-sequential formal dynamic modal logic Cannonical version of .See [Lamport91] TLA Temporal Logic of Actions. .Close Lamport94c .Open Lamport94c Leslie Lamport Writing Proofs Microsoft Research .See http://research.microsoft.com/en-us/um/people/lamport/proofs/proofs.html =IDEA PROOFS FORMULAS STRUCTURED FORMAL LOGIC MATHEMATICS Published off line as .See [Lamport95] below. .Close Lamport95 .Open Lamport95 Leslie Lamport<lamport@src.dec.com> How to Write a Proof American Math Monthly V102n7(Aug-Sep 1995)pp600-608 =DEMO PROOFS FORMAL LOGIC .Box Hierarchically structured proofs in outline style see Abadi & Lamports work. Q.E.D. is a step representing what needs to be proved: .As_is Theorem <statement> .As_is PROOF SKETCH: <english style proof scetch> .As_is ASSUME: <label>. <predicate> ... .As_is PROVE: <predicate> .As_is NumberedList( <number>. <step|predicate> ) .As_is <number>. Q.E.D. .As_is LET: <definitions> .As_is Choose .... such that.... .As_is CASE: statement of assumption is short for .As_is ASSUME: Statemnt of assumption .As_is PROVE: Q.E.D. .Close.Box Also see online reports .See [Lamport94c] .Close Lamport95a .Open Lamport95a Leslie Lamport TLA in Pictures IEEE Trans SE VSE-21n9(Sep 1995)pp768-775 =THEORY TLA Formal Graphics temporal logic of actions .Box Claims: first use of diagrams to provide complementary multiple formal views. an aid to presenttion and proof. Like FSA(states=>predicates, transactions => actions) out(n):edges out of n, d(e) :nodes=destination of edge e, P(n) :=predicate on node n, P'(n) :=primed predicate... disjoint_predicate:=for all nodes n1,n2(not(P(n1) and P(n2)). A(n) :=for some e:out(n)(action(n) and P'(d(e))) two possible formula for meaning of transitions: \Delta:=for all nodes n, always(if P(n) then A(n) ) or \Delta_bar:=always(some nodes n(P(n) and A(n))). ()|- if \Delta then \Delta_bar ()|- if disjoint_predicates then (\Delta iff \Delta_bar) .Close.Box .Close LamsweerdeDarimontLetier98 .Open LamsweerdeDarimontLetier98 Axel van Lamsweerde & Robert Darimont & Emmanuel Letier Managing Conflicts in Goal-Driven Requirements Engineering IEEE Trans SE V24n11(Nov 1998)pp908-926 =THEORY PURPOSE KAOS LIGHTWEIGHT FORMAL temporal LOGIC views Some EXPERIENCE find scenarios leading to divergences. Obstacles are scenarios that make it impossible to meet all the requirements .Close LamsweerdeLetier00 .Open LamsweerdeLetier00 Axel van Lamsweerde & Emmanuel Letier Handling Obstacles in Goal-Oriented Requirements Engineering IEEE Trans Software Engineering V26n9(Sep 2000)pp978-1005 =CASESTUDY REQUIREMENTS REFINEMENT EXCEPTIONS TEMPORAL LOGIC KAOS Requirements can assume too much reliability in parts of system. Should calculate things that can go wrong and allow for them in their requirements. p983: "an obstacle defines a set of undesirable behavior; a negative scenario produces a behavior in this set". Obstacles imply a goal is not met but obstacles must not be inconsistent with the domain - exists a scenario Goals have form "at all times...." but obstacles have form : "at some time...." .See [KjaerMadsen95] `user anti-story`! .Close LamsweerdeWillemet98 .Open LamsweerdeWillemet98 Axel van Lamsweered & Laurent Willemet Inferring Declarative Requirements Specifications from Operational Scenarios IEEE Trans SE V24n12(Dec 1998)pp1089-1114 =DEMO USER to PURPOSE TLA FORMAL LOGIC LANGUAGE KAOS WHY+WHO+WHEN+WHAT Lift Stakeholders may have problems expresssing requirements in abstract but typical scenarios are easier to elicit. SCENARIO as example of or counter-example to abstraction Scenario=sequence diagram, Goal.types={achieve, Cease, maintain, avoid}. .Close LangeChaudronMuskens06 .Open LangeChaudronMuskens06 Christian F J Lange & Michel R V Chaudron & Johan Muskens In Practice: UML Software Architecture & Design Description IEEE Software Magazine V23n2(Mar/Apr 2006)pp40-46 =POLL 80 Architects +14 CASE STUDIES UML QUANTITY QUALITY METRICS 80% used usecase & logical, 50% component & scenarios, 17% deployment. Loose adherence to standard. Survey presumed a "waterfall" process. Problems mentioned in poll. scattered information, incompleteness, disproportion, inconsistency, diagram quality, informality, no conventions. 40%+ plan to use more UML metrics. Defects in case studies: classes do not fit sequence diagrams, classes with no methods. Experiment: most students & practitioners can't detect mismatches between class and sequence diagrams. See "Effects of defects in UML models" in ICSE06 by Lange & Chaudron. .Close LanoGoldsackSanchez99 .Open LanoGoldsackSanchez99 Kevin Lano & Stephen Goldsack & arturo Sanchez specification of a Chemical Process Controller in B In .See [HincheyBowen99] pp53-80 =EXPERIENCE fORMAL SPECIFICATION REACTIVE VALIDATION V&V B PCT FSM TEMPORAL LOGIC StateCharts TOOLS Chemical process control synthesis. Worked but would have liked to have temporal logic to specify dynamics .Close LemosSauudAnderson92 .Open LemosSauudAnderson92 R de Lemos & A Sauud & T Anderson A Train Set as a Case Study for the Requirements Analysis of Safety Critical Systems Computer Journal V35n1(Feb 1992)pp30-40 CR9307-0516 =CASE-STUDY REQUIREMENTS Reality .Box Faults in Requirements cause disasters Separate the mission from safety requirements distinguish Physical Reality from System Use logic for R and Petrie Nets for System. Timed History Logic .Close.Box .Close Lenat95 .Open Lenat95 Douglas B. Lenat(mailto:Lenat@MCC.COM & doug@cyc.com) CYC: A Large-scale Investment in Knowledge Infrastructure Commun ACM V38n11(Nov 1995)pp33-38 +pp45-48(critiques) =EXPERIENCE CYC LOGIC ONTOLOGY .Close Lenatetal90 .Open Lenatetal90 Douglas B. Lenat & R.V. Guha & Karen Pittman & Dexter Pratt & Mary Shephard Cyc: Toward Programs with Common Sense Commun ACM V233n6(Aug 1990)pp30-49 =EXPERIENCE CYC LOGIC ONTOLOGY .Close LetierLamsweerde02 .Open LetierLamsweerde02 Emmanuel Letier & Axel van Lamsweerde deriving Operational Software specifications from System Goals SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp119-128 =DEMO SYSTEM REQUIREMENTS GOAL REFINEMENT PATTERNS LOGIC AND/OR TEMPORAL RT-LTL REALITY ENTITY RELATIONSHIP OPERATION SPECIFICATION An operation is a temporal proposition defined by the current truth of a set of preconditions and the truth in the next step of a set of postconditions. goal_patterns::=achieve | maintain_avoid. achieve::= unbounded_achieve | bounded_achieve | immediate_achieve. unbounded_achieve: for always if C then sometime T. maintain_avoid::= state_invariance | transition_invariance. state_invariance::=global_invariance | after_invariance | in-between_invariance. .Close Lev-AmiEtal00 .Open Lev-AmiEtal00 Tal Lev-Ami & Thomas Reps & Mooly Sagiv & Reinhard Wilhelm Putting Static Analysis to Work for Verification: A Case Study Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp26-38 =DEMO TOOL PROOF POINTERS 3-valued LOGIC GRAPH .Close LewisT94d .Open LewisT94d Ted G Lewis(<lewis@cs.nps.navy.mil>Naval Postgraduate School) The Next 10000[2] Years: Part II IEEE Computer Magazine V29N5(May 1996)pp78-86 =ESSAY predictions DESIGN REUSE .Box Note 10000[2]years = 16.years, Continues .See [LewisT94c] networks will survive. Software as Steam for the future. Quotes Capers Jones on programmer productivity increasing 3-5% per year ($/fp). Shows comparison of power of languages. reates an oportunity for new ideas etc. Predicts large MIS will go for visual tools and object tools rather than languages. (compare Keuffel96? - the bubble sort effect). OT as a stepping stone, discarding functional decomposition and hiding if-then-else logic. Errors of inheritance and polymorphism. Things lacking and possible fixes: .Box Requirements: continuous adaption defects: correct-by-construction Avoid big systems, make pieces Time: paint programs Cost: throwaway parts expertise: use tools with artistic skills needed .Close.Box Frameworks with API, Components produced by experts. Applets as event handlers with user in control using frameworks and components .Close.Box .Close Li91 .Open Li91 Xiaofeng Li What's so Bad about Rule-Based Programming IEEE Software V8n5(Sept 1991)pp103-105 =DEMO LOGIC PROGRAMMING AI Technical Maintenance Reliability .Close LichtensteinPnueli00 .Open LichtensteinPnueli00 Orna Lichtenstein and Amir Pnueli Propositional Temporal Logics: Decidability and Completeness Logic Journal of the IGPL V8n1(Jan 2000)pp55-85 .See http://www3.oup.co.uk/igpl/Volume_08/Issue_01/#Lichtenstein =THEORY FORMAL LOGIC TIME PTL =HISTORY 20 years axioms etc complete and sound relative model, decision procedure using semantic tableau. time with a beginning. Basic modal operators: Next, Until, Weak_previous, Since. Defines half-a-dozen others. .See http://csci.csusb.edu/dick/maths/logic_9_Modalities.html#PTL .Close Lifschitz95 .Open Lifschitz95 Vladimir Lifschitz The Logic of Common Sense ACM Computer Surveys V27n3(Sep 1995)pp343-345 =SURVEY AI Logic defaults inertia .Box Quotes and refers to Leibnitz's "An Introduction to a secret Encyclopedia": "Everything is presumed to remain in the state in which it is" The commonsense law of inertia .Close.Box .Close LocascioDarpel93 .Open LocascioDarpel93 Capt Charles J Locascio & 2Lt Mathew M darpel Software Reengineering for the Future with Ada IEEE Computer Society Reverse Engineering Newsletter n5&6(Dec 1993)pp4-5 =EXPERIENCE LEGACY COBOL JCL RENGINEERING Ada DFD REQUIREMENTS .Box Replacing13 year-old undocumented suite of COBOL programs and JCL Into Ada Analysis of JCL+COBOL, JCL->physical DFD->Logical DFD = 4 diagrams! cf results with Requirements-> missing, extra, obsolete preliminary oo design: real world objects Prelimnary Object Encyclopedia" OOD Advanced CASE Technology Design Based Maintenance(DBM) : Design+Code is one thing. Teamwork DSE(Design sensitive Editor) Ada Structure Graphs(ASGs) reuse: Booch components, 100s of generic packages, domain library Ada Helped. .Close.Box .Close Long78 .Open Long78 Chris Long Logical =LETTER ENGLISH LOGIC ITL UNIVERSAL LANGUAGES Computer Weekly (UK) (Mar 16 1978)p20 You can write English logically! .Close Lover08 .Open Lover08 Robert Lover Elementary Logic: for software Development Springer Publishing NY NY (2008) ISBN 1848000812 $CR 1002-0125 =UNREAD =TEXT LOGIC Notes .Hole Lover08 .Close LupuSloman99 .Open LupuSloman99 Emil C Lupu & Morris Sloman Conflicts in Policy-Based Distributed Systems Management IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp82-867 =THEORY TOOL SYSADMIN MODAL LOGIC distinguishes policies that permit actions(A+), forbid actions(A-), require actions(O+ on event), require non-action(O-), O:=Obligation, A:=Authorisation. .Close MacLennan79 .Open MacLennan79 B. J. MacLennan Observations on the Differences Between Formulas and Sentences and their Application to Programming Language Design SIGPLAN V14n7 (Jul 1979)p51-61 =DEMO logic languages graphic .Close Maddux96 .Open Maddux96 Roger D Maddux Relation-algebraic semantics Theor Comp Sci V160n1-2(Jun 1996)pp1-85 =SURVEY LOGIC SEMANTICS REGULAR-EXPRESSIONS meaning of a statement is two elements in a relation algebra. One element defines what happens if the statement terminates and the other defines the states when the statement will not terminate. cf .See [Hoareetal87] .Close Maiden08a .Open Maiden08a Neil Maiden Requirements 25 years on IEEE Software Magazine V25n6(Nov/Dec 2008)pp26-28 =HISTORY 1983-2008 REQUIREMENTS 14 references 1970s: Requirements were monolithic and used natural language with "noise, silence, contradiction, ambiguity, and wishful thinking". VDM .See [Bekic70] and JSP .See [Jackson75] available but not used. Pencil and Paper 1977: Ross .See [Ross77] developed SADT notation (IDEF) and method .See [Ross85] and story telling. 1978: .See [Jackson78] System maintains a model of reality. Leads to JSD in the 1980s 1979: DeMarco .See [DeMarco79] , Gane&Sarson .See [GaneSarson79] , Yourdon .See [Yourdon75] & Constantine. DFDs. Logical vs Physical. STDs. Functional decomposition. Informal diagrams. structured analysis and design. First CASE tools help draw informal graphics. 1980s: Greenspan. .See [BorgidaGreenspanMylopoulos85] .See [BorgidaGreenspanMylopoulos94] Semantic networks, logic, frames model knowledge about situation. RML: the model is collection of objects of different types. Ontology: entities, activities, assertions. Leads to TROPOS, i*, KAOS (Knowledge Acquisition in Automated Specification). Goals and Constraints. Expert systems. 1980s: Stakeholders have difficulties articulating requirements. So, repertory grids, card sorting, Laddering. .See [Maiden09] 1990s: Ethnography, HCI. Complexity of the working environment. 1998: Beyer & Holtzblatt .See [BeyerHoltzblatt94] .See [BeyerHoltzblatt95] : Contextual enquiry. 1999: Vicente: Cognitive work Analysis 2004: .See [MaidenGizikisRobertson04] : Inventing requirements. Today: better at identifying stakeholders, use cases and scenarios, quality requirements, reasoning about natural language, multiply viewpoints, detecting and handling conflicts, social techniques, Tracing requirements, tailoring to different domains, training analysts. Meanwhile: We are tackling larger and more complex systems. Also see .See [Maiden05] on requirements research. .Close MaidenGizikisRobertson04 .Open MaidenGizikisRobertson04 Neil Maiden & Alexis Gizikis & Suzanne Robertson Provoking Creativity: Imagine what your Requirements Could Be Like IEEE Software Magazine V21n5(Sep /Oct 2004)pp68-75 =EXPERIENCE REQUIREMENTS WORKSHOP CREATIVITY CORA RESCUE Pre-USE CASE Describes theoretical basis for creative thinking: Diverge; Converge. Prepare, incubate, illumination, verification. Cf. CORT TEC Target-Expand-Contract RESCUE::="Requirements Engineering with Scenarios for User-centered Engineering". CORA::="COnflict Resolution Assistant", for air-traffic Control. Cf. TCAS projects. Used other domains and analogies to explore requirements. Analogy via a common abstraction. Combine random stimuli(eg toy frog) and combinations of requirements. Transform problems by relaxing constraints. Helps to understand the difficulty of creativity. Encourage playfulness. Groups and plenary sessions. Ideas on cards. Analogies need a step-by-step guidance. It takes time to incubate analogical ideas, Structure workshops about ideas rather than creative processes. Record the rationale behind ideas. Time to let off steam... Plan plan and then plan alternatives. Need a champion for workshops. See Gottesdiener, DeBono, Wickelgreen, ... .Close Makinson08 .Open Makinson08 David Makinson Sets, Logic, maths for computing Springer NY NY 2008 ISBN 1846288444 =UNREAD DISCRETE MATHEMATICS Notes .Hole Makinson08 .Close Malik11 .Open Malik11 Petra Malik A retrospective on CZT Software & Experience 41(2): 179-188, 2011. =EXPERIENCE F/OSS OPEN SOURCE TOOL FORMAL Z Requirements specification verification tools LOGIC Set Theory UNICODE XML Circus Community Z Tools on SourceForge. See .See http://en.wikipedia.org/wiki/Community_Z_Tools on the Wikipedia. .Close MannaPnueli91 .Open MannaPnueli91 Zohar Manna & Amir Pnueli Completing the temporal Picture Theor Comput Sci V83n1(Jun 1921)pp97-130 .See [CR] 9204-0235 =THEORY LOGIC SPECIFICATION MODAL TEMPORAL ASSERTIONAL If a safety, response, or reactivity property can be proved in temporal logic then it can be proved in assertional logic .Close MannaPnueli92 .Open MannaPnueli92 Zohar Manna & Amir Pnueli The Temporal Logic of Reactive and Concurent Systems: Systems Springer Verlag NY NY 199? =THEORY MODAL TEMPORAL LOGIC .Close MannaWaldinger85 .Open MannaWaldinger85 Zohar Manna & Richard Waldinger The Logical Basis for Computer Programming: Vol 1 Deductive reasoning Addison Wesley series in C Sci 1985 =TEXT logic .Close Mankin78 .Open Mankin78 R Mankin Loglan -- a more flexible language =LETTER Esperanto vs Loglan Volapuk LOGIC ITL UNIVERSAL LANGUAGES Computer Weekly (UK) (Apr 13 1978)p16 Argues that an ITL must be artificial so that it does not grow, adapt, and develop dialects! Rebuttal: Esperanto is used widely and yet has no dialects. .Close Markus83 .Open Markus83 M Lynne Markus Power, Politics, and MIS Implementation Commun ACM V26n6(Jun 1983)pp430-444 & .See [MyersAvisson02] Chapter 3, pp19-48 =EXPERIENCE PEOPLE SYSTEMS RESISTANCE POLITICS ORGANIZATION MANAGEMENT FIS In this case People resisted a new system not just because it wasn't good enough, or because they were not trained etc, but because the new Financial Information System was a ploy to change the organization. New FIS system tended to move data and power toward a centralized system and away from divisional centers. Divisions fought the system. Sometimes it is better to change the organization first and then change the technological systems in use. .Close MassonetLamsweerde97 .Open MassonetLamsweerde97 Phillipe Massonet & Axel van Lamsweered Analogical Reuse of Requirements Frameworks .See [RE'97] =ADVERT KAOS SPECIFICATION LANGUAGE ontology temporal logic graphic tool .Close MathewsMcGee90 .Open MathewsMcGee90 Robert W Matthews & William C McGee Data Modeling for Software Development IBM Systems Journal V29n2(1990)pp228-235 =DEMO Conceptual vs Logical vs Physical p233 orthogonal to Zachman .Close MattoliniNesi01 .Open MattoliniNesi01 Riccardo Mattolini & Paolo Nesi An Interval Logic for real-Time system Specification IEEE Trans Software Engineering V27n3(Mar 2001)pp208-227 =THEORY MATHEMATICAL LOGIC TEMPORAL SPECIFICATION LANGUAGE TILCO .Close MayhewMGouHaaseHartemink12 .Open MayhewMGouHaaseHartemink12 Michael B Mayhew & Xin Guo & Steven B Haase & Alexander J Hartemink Close encounters of the collaborative kind IEEE Computer Magazine V45n3(Mar 2012)pp22-30 =ARTICLE ANALYSIS DESIGN ITERATION BIOLOGY YEAST DOMAIN LANGUAGE Describes a collaborative development of software for modeling a biological process and answering biological questions about it. Illustrates need to find and develop a common language for the stakeholder's domain. Need to answer biological questions. In general: make sure you know what the user's want. Whu not use cases? Process was iterative. .Close McCamantErnst03 .Open McCamantErnst03 Stephen McCamant & Michael D Ernst Predicting Problems Caused by component upgrades FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp287-296 =DEMO MODULE TESTING LOGIC CONTRACT V&V EVOLUTION Daikon Simplify PERL Before putting an upgraded component into an application, use the application+old component to generate a mathematical contract for the old component, then derive a similar contract for the new one. Only safe if the new contact is stronger than the old one. contracts::=$ Net{ pre, post: @States}. For contracts c1, c2, c1 is_stronger_than c2 ::= (c1.pre ==> c2.pre) and ((c1.pre&c2.post)==> c1.post). Worked well on to PERL module upgrades! Nice example of upgrading swap: will work in a bubble sort, but not in a particular selection sort. .Close McCannRoman98 .Open McCannRoman98 Peter J McCann & Gruia-Catalin Roman Compositional Programming Abstrations for Mobile computing IEEE Trans Soft Eng V24n2(Feb 1998)pp97-110 =ADVERT non-sequential Net/Web LANGUAGES(UNITY) LOGIC PROOF .Close McCannRoman99 .Open McCannRoman99 Peter J McCaqnn & Gruia-Catlin Roman Modeling Mobile IP in Mobile UNITY ACM TOSEM V8n2(Apr 1999)pp115-146 =CASESTUDY MOBILE UNITY LOGIC PROOF Protocol .See [McCannRoman98] .Close McCarthy87 .Open McCarthy87 John McCarthy Generality in Artificial Intelligences Commun ACM V30n12(Dec 1987)pp1030-1035 based on 1971 Turing award talk =ESSAY AI LOGIC LPC not PROLOG situation calculus frame problem nonmonotonicity. Similar problems arrise in formal specifications: .See [Borgidaetal95] .Close McClintock97 .Open McClintock97 Colleen McClintock The Logic of Business Rules Software Development magazine V5n11(Nov 1997)pp44-48+50 =DEMO DATA REALITY LOGIC CORBA IDL DATA encodes REALITY LOGIC: repository to collect formulate store and maintain rules(Rochade/Microsoft/Platinum) hence models diagrams executable(CORBA IDL) rule servers .Close McRae02 .Open McRae02 Eric McRae Tracking Down Killer Bugs Dr. Dobbs #335(Apr 2002)pp58+60-61+63-64 =EXPERIENCE EMBEDDED DEBUGGING TPU AUTOMOTIVE microcode ashware finding an unpredictable hard/software bug close to the deadline in code controlling a motor. Test platform for debugging cost $3500 -- real time simulators of environment and system + logic analyzer. +$700 for Linux compatible debugger. Bug found by inspiration, data gathering, hardware simulation and monitoring, plus *explaining* the situation in detail. .Close Mercurioetal90 .Open Mercurioetal90 V J Mercurio & B F Meyers & A M Nisbet & G Radin AD/Cycle Strategy and Architecture IBM Systems Journal V29n2(1990)pp170-188 =ADVERT METHODS AD/Cycle IBM .Box p172-173: model..specs...logic+screens+DB I/O, Build, Install, Maintain (Software Magazine field report September 1993) |- IBM abandons AD/Cycle as a main frame product. .Close.Box .Close MetayerEtAl11 .Open MetayerEtAl11 Daniel Le Metayer & Manuel Maarek & Eduardo Mazza & Marie-Laure Potet & Stephane Frience & Valerie Viet Triem Tong & Nicolas Craipeau & Ronan Hardouin Liability Issues in Software Engineering: the use of formal methods to reduce legal uncertainties Commun ACM V54n4(Apr 2011)pp99-106 .See http://doi.acm.org/10.1145/1924421.1924444 =DEMO MASS MARKET SOFTWARE CONTRACTS LOGIC TOOLS CHECKING EULA Shows how symbolic logic can be used to clarify who is responsible for various bad things happening. formal model in terms of mappings `time stamps` ->@( {`Send`, `Receive`} >< (`Components` | `Users` )^2 >< `Data`). Example: A document is only received if it has been sent: For all documents d ( (`Receive`, `Serv`, `SigApp`, d) in T(\theta) iff (`Send`, `SigApp`, `IO`, d) ). Liability maps `Claims`><`Traces`><\theta -> @(`Parties`). .Close Meyer85 .Open Meyer85 Bertrand Meyer On Formalism in Specification IEEE Software V2n1(Jan 1985)pp6-27 =DEMO formal logic non-sequential PURPOSE Reality .Box Examines line breaks problem, notes structure clash and use of pipes and inversion for solution. inspiration for my 'br' program: .See http://www/dick/tools/br.d.html .Close.Box .Close Mills75 .Open Mills75 Harlan D Mills The New Math of Computer Programming Commun ACM V18n1(Jan 1975)pp43-48 =THEORY MATH LOGIC structured CLEANROOM Also presented paper that year on getting programs right. International Conference on Reliable Software.(Berard) Refed in Zelkowitz90, cites .See [BohmJaccopini66] .Close MorrisBunkenburgTyrrell09 .Open MorrisBunkenburgTyrrell09 JOSEPH M. MORRIS & ALEXANDER BUNKENBURG & MALCOLM TYRRELL Term Transformers: A New Approach to State ACM Trans. Program. Lang. Syst. V31n4 (May 2009)a16:1-42 .See http://doi.acm.org/10.1145/1516507.1516511 =IDEA TERM TRANSFORMERS PREDICATE wp LANGUAGES SEMANTICS LOGIC PROOF Lambda axiomatic denotation Dijkstra phase ::=command "|>" term. In the text \righttriangle is used for my "|>" above. Example: x:=x+1 |> x^2 = (x+1)^2. Uses a lambda calculus based language of commands and terms to establish mathematical `bona vides`. .Close MorzentiSanPietro .Open MorzentiSanPietro Angelo Morzenti & Pierluigi San Pietro Object-oriented logical specification of time-critical systems TOSEM V3n1(Jan 1994)pp56-98 CR9503-0166 =THEORY OBJECT_ORIENTED LOGIC SPECIFICATION TIMING .Close MoserEtal97 .Open MoserEtal97 L E Mose & Y S Ramakrishna & G Kutty & P M Melliar-Smith & Laura K Dillon A Graphical Environment for the Design of Concurrent Real-Time Systems ACM TOSEM V6n1(Jan 1997)pp1-30 =THEORY GRAPHIC LOGIC SPECIFICATION TIMING RTGIL::=Real-time Graphical Interval Logic .Close MunakataJani94 .Open MunakataJani94 Toshinori Munakata & Yashvant Jani Fuzzy Systems: An Overview Comm ACM V37n3(Mar 1994)(AI issue)pp69-76 =SURVEY =ADVERT FUZZY LOGIC MATHEMATICS .Close MyersJP90 .Open MyersJP90 J. Paul Myers Jr. The Central Role of Mathematical Logic in Computer Science ACM SIGCSE V22n1(Feb 1990)pp22-26 =ESSAY logic formal .Close Nagel56 .Open Nagel56 E Nagel A Formalization of Functionalism Logic Without Metaphysics Free Press 1956 pp247-283, reprinted Emery69 =ESSAY FUNCTION SYSTEMS PURPOSES p298. distinguishes mathematical function from purpose. p311. functional analysis in social systems requires a standardized/patterned/repetitive items .Close Naur07 .Open Naur07 Peter Naur Computing versus Human thinking Commun ACM V50n1(Jan 2007)pp85-94 + letter V50n4(Apr 2007)pp7-8 =HISTORY REJECTING MODERN PSYCHOLOGY LOGIC TURING AI vs plastic neural nets $CR 0801-0095 William James Science as description not theorizing. .Close NaumovichClarke00 .Open NaumovichClarke00 Gleb Naumovich & Lori A Clarke Classifying Properties: An alternative to the Safety-Liveness Classification .See [FSE8] pp159-168 =IDEA TEMPORAL LOGIC SPECIFICATION ANALYSIS SAFETY LIVENESS classifies properties in terms (1) that describe finite, infinite, or both kinds of sequences events, pus (2) that must be checked on finite, infinite, or both kinds of sequences of events. .Close Nicollinetal92 .Open Nicollinetal92 Xavier Nicollin & Joseph Sifakis & Sergio Yovine Compiling Real-Time Specifications into Extended Automata IEEE Trans SE-V18 n9 (Sep 1992)pp794-804 =THEORY timeout watchdog gnerates event driven FSM from logical specification .Close NentwichEtAl03 .Open NentwichEtAl03 Christian Nentwich & Wolfgang Emmerich & Anthony Finckelstein & Ernst Ellmer Flexible Consistency Checking ACM TOSEM Trans Software Eng & Methodology V12n1(Jan 2003)pp28-63 =DEMO WEB/NET DOCUMENTATION XML xlinkit webservice LOGIC CONSISTENCY MANAGEMENT DIFFERENCING TOOL UML Java EJB Links are not placed in documents. Connect elements in other documents. Four kinds of constraint: standard, extension, integration, custom. xlinkit::webservice=http://www.xlinkit.com. .Close Nishidaetal91 .Open Nishidaetal91 Fujio Nishida & Shinobu Takamatsu & Yoncharu Fujita & Tadaaki Tani Semi-Automatic Program Construction Using Library Modules IEEE Trans SE-17 n9 (Sep 1991)pp853-871 CR9302-0087 =THEORY re-use logic natural PURPOSE MAPS \equiv MATHS refinement := unification and proof by refutation of horn clauses of structured specification with problem parts library with specifications. .Close Nissanke99 .Open Nissanke99 Nimal Nissanke Introductory Logic and Sets for Computer scientists Addison Wesley Longman 1999 ISBN 0-201-17957-1 QA76.9 L63N57 =TEXT Z LOGIC DISCRETE MATH for CSUSB csci556/656 .Close OConnell02 .Open OConnell02 Laurie O'Connell Communications Gap Software Development Magazine V10n5(May 2002)pp17 =REPORT SOFTWARE QUALITY Reports on a 10 year DoD "National software quality Experiment" in the "Software Inspection Lab". No appreciable reduction in errors or improvements in process. Main defects noted: 41% lack of traceability, 23% infringing standards. 7% logic errors. 7% functionality. 5% syntax. 5% initial values. 4% maintainability. Software products are not "well connected" to their business requirements. .Close Okrent09 .Open Okrent09 Arika Okrent In the Land of Invented Languages: Esperanto Rock Stars, Klingon Poets, Loglan Lovers, and the Mad Dreamers Who Tried to Build A Perfect Language Random House Publishing Group Pub. Date: May 2009 ISBN-13: 9780385527880 352pp =SURVEY =HISTORY 900 ARTIFICIAL LANGUAGES Blissymbolics MATHEMATICS LOGIC Elvish Esperanto Gestuno Wilkins thesaurus Dalgarno Zamenhoff ONTOLOGY Repeatedly somebody has had the same ideas for improving on natural "grown" languages -- using logic, setting up an ontology, using symbols, using numbers, using european languages, etc. There is no natural ontology/symbology/adamic language. Humans evolve the language that they use. Language inventors come into conflict with language users. Bliss symbols for disabled children -- students needs vs Bliss's obsessions. Loglan vs Lojban. Brown vs the Loglanists. Writing Lojban is like programming. Speaking it seems to be impossible. Learning a new language leads you to see the world differently. Benjamin Whorf's Hypothesis? Didn't mention e-prime or SLUNT... You thoughts can go here: .Hole .Close OrtinEtal04 .Open OrtinEtal04 Francisco Ortin & Benjamin Lopez &J Baltasar Garcia Perez-Schofield Separating Adaptable Persistence Attributes through computational Reflection IEEE Software Magazine V21n6(Nov /Dec 2004)pp41-49 =DEMO TOOL SEPARATE PERSISTENCE DATA vs BUSINESS LOGIC Nitr0 Java REFLECTION Notes .Close Owreetal95 .Open Owreetal95 Sam Owe & John Rushby & Natarajan Shankar & Friedrich von Henke Formal Verification for Fault-Tolerant architectures: prolegomena to the Design of PVS IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp107-125 =ESSAY FORMAL LOGIC TOOL partial functions SPECIFICATION PVS::=http://www.csl.sri.com/pvs.html, `System for generating proofs`. .Box PVS next generation after EHDM(1984) interactive uses ASCII input plus map to LaTeX and graphics, under EMACS ftp://ftp.csl.sri.com/pub/pvs Application to concurrent faulty systems. p114: "Most of the proofs ... not to mention many of the theorems and some of the algorithms wer incorrect when we started... our axiomatizations were occassionally unsound, and sometimes they were sound but did not say what we thought they did... our verifiactions are seldom finished: changed assumptions and requirements, the desire to improve an argument or a bound, and simple experiementation, have led us to revise some or all of our verifiactions several times... [they are used] by someone other than their original developer.....structured....modular" "we found that substantial effort was expended on the formal development of 'background theories' such as summations, bitvectors, finite sets, and so on. Clearly, it is necessary that such theories should be made available in libraries for future reuse." Help in debugging specifications. working(r):set[R]={r | member(c, OK(r))}. p118: "Some specification environments allow specifications to be expressed directly in terms of mathematical symbols[...]we have found that the burden of supporting these conveniences outway the benefits, bringing in the wake such menaces to productivity as structure editors, and a plethora of mouse and menu selections. In the US, at least, most scientists and engineers are fast touch typists, and we ind a conventional program editor provides a more productive environment for rapid interaction than a graphical user interface[...]LaTeX,...graphical representation of module dependencies and proof trees...hypertext" .Close.Box .Close PahlCasey03 .Open PahlCasey03 C Pahl & M Casey Ontology support for web service processes FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp208-216 =FORMAL WEB/NET LOGIC ALGEBRA LTS Kripke temporal description LANGUAGES Many definitions, no results. .Close Pappas92 .Open Pappas92 T.L.(Frank) Pappas Logical Document Design with Scientific Word IEEE Computer V25 n8(Aug 1992)p85 =Review TOOL WRITING MATHEMATICS LOOK_AND_FELL vs SEMANTIC STRUCTURE TAG Chapter 3: lexical and output formatting. .Box Quote "When writing a paper, you should only be concerned with such issues as identifying section headings, stating theorems, providing bibliographic citations, and making reference to other potions of the paper. These have nothing to do with the papers appearance, which varies with the style used by the journal it will appear in." "tags" marker: <id> <-----< ref: <id> .Close.Box .Close Parnas77 .Open Parnas77 David Lorge Parnas Co-Routines and Networks of Parallel Processes Proc IFIP 77 (North Holland Pub Co 1977) pp861-867 (invited paper) =IDEA MATHEMATICAL TOP-DOWN SPECIFICATION LOGIC DESIGN .Close Parnas93 .Open Parnas93 David Lorge Parnas Predicate Logic for Software Enginering IEEE Trans software Engineering SE-V19n9(Sep 1993)pp856-862 =EXPERIENCE FORMAL SPECIFICATION LOGIC partial functions .Box Problem with partial functions in specification. example: sqrt, subscript, ... Simple fix for engineering purposes: state that primitive predicates have the value false when an argument is undefined. A primitive predicate is one that (1) has values defined for all defined arguments, (2) is not defined in terms of any other predicate, (3) is false if any argument is undefined. Not unsimilar to the Logic of Partial Terms: .See [LPT]. Also see .See [PVS] .Close.Box .Close Parnas96a .Open Parnas96a David Lorge Parnas Mathematical Methods: What we need and don't need IEEE Computer Magazine V29N4(Apr 1996)pp28-29 =ESSAY MATHEMATICS ENGINEERING model description specification .Box not "formal" but "mathematical", as in other areas of engineering. part of the everyday toolset current are theoretically sound but hard to use littered with sound foundations on which nobody has erected a useful edifice more work on notation - current is cumbersome and hard to use. distinguish: model, description, and specification. unreasonable focus on proof of correctness more tme spent applying and improving methods, not selling them, They've been used ( .See [Parnas94] ...) but not using symbolic logic. .Close.Box .Close Parnas10 .Open Parnas10 David Lorge Parnas Really rethinking 'Formal Methods' IEEE Computer Magazine V43n1(Jan 2010)pp28-34 + letter V43n3(Mar 2010)pp6-7 =POLEMIC =HISTORY FORMAL METHODS ASSUMPTIONS RESEARCH vs PRACTICE MATHEMATICS ENGINEERING vs PHILOSOPHY Claims of progress and industrial adoption doubted. Example: benefits of inspection vs formal specification known since 1979. They can account for most later claims! Alarming gaps: Research vs Practice, Software development vs engineering, computer science and mathematics. Mathematical papers are about a particular formal language not discovering ways to apply new mathematics to a problem. Computer variables are finite state machine but in mathematics variable are placeholders in functions and relations. How to handle arrays. Conventional expressions don't express piecewise-continuous and discrete functions. These days: most software variables have a hidden state., programs do not terminate, and time is important. Use relations and relational algebra! Abandon pre-conditions and post-conditions! Work in multiple directions. Find ways to handle side-effects and non-determinism. Distinguish model vs specification vs description. Avoid "specification languages" Investigate using a predicate to specify requirements. Need to be able to analyze a program like an engineer analyses a circuit. Not program proof, but derivation of properties. Need to research ways to use mathematics to document programs -- outside of the code of the program. De-emphasize "technology transfer" and advocacy, instead go back and change what we are selling. We need an integrated notation and step by step ways of moving from user to code. Be careful to spot abstractions that are lies! Don't try to be philosophers and logicians... try to emulate engineers. Letter from Toomas Plaks: Some math applications were lost in the search for formal methods. Letter from Lee Pike: quotes examples of successful FMs, but some research not worthwhile. Reply: mathematics is not yet mainstream. .Close Parnas10a .Open Parnas10a David L Parnas Inside RISKS: Risks of Undisciplined development Commun ACM V53n10(Oct 2010)pp2527- .See http://doi.acm.org/10.1145/1831407.1831419 =ESSAY ENGINEERING DISCIPLINE vs SLOPPY PROGRAMMING SOFTWARE BUGS Engineering designs must be fit for their purpose, conform to standards, handle all foreseeable circumstances (including human error), and be designed with a margin of error for safety. Anecdotes of typical problems with software. Proposes .List First Describe all possible inputs. Second express requirements as disjoint sets of inputs with a common simple rule. Then verify no overlaps, and each output is correct in the opinion of stakeholders. Use simple logic. Complications: (1) often need to work with sets of sequences of inputs. (2) Function names? (3) Output rule may be complex. .Close.List Situation won't change if customers don't stop buying sloppy software. .Close Parnasetal94 .Open Parnasetal94 David Lorge Parnas & Jan Madey & Michal Iglewski Precise Documentation of Well Structured Programs IEEE Trans SE VSE-20n12(Dec 1994)pp949-976 =EXPERIENCE RISKS TABULAR RELATION DOCUMENTATION V&V The Darlington Project: verify safety of large atomic reactor shutdown program Use tables not symbolic logic. Specify the Before-After relationship and the conditions when it will not fail to terminate. a_display::=Net{ this_part_s_spec:specification; this_part_s_structure:structure; components:#specification}, shows what you need to validate a part. .See http://www/dick/notes/Parnasetal94.html .Close PascalF04 .Open PascalF04 Fabian Pascal Data management misconceptions Government Computer News V23n9(Sep 2004) .See http://gcn.com/23_29/interview/27383-1.html =INTERVIEW HARMFUL XML SQL XML retransmits redundant tags with each set of data transmitted. XML is no more than a hierarchical database when used for storage. XML does not provide integrity checks of a relational system. XML does nothing to provide the logic/mathematics provided by previous data management systems. SQL allows duplicated entries and empty entries in a table and so allows errors and forces work arounds. SQL implementations are often incomplete and inefficient.... making it worse. .Close Paulos98 .Open Paulos98 John Allen Paulos Once Upon a Number: The Hidden Mathematical Logic of Stories Basic Books NewYork NY 1998 ISBN 0-465-05158-8 QA276.P285 =ESSAY LOGIC MATHEMATICS and story telling Differences between informal logic and formal logic. The importance of taking a point of view or placing data in a story-like context. Note: Software is a formal system thrown into an informal context. Choice can change the odds in such a way as to invalidate the choice! Ramsey-type theorems: In a large enough sample even unlikely events will occur. The Delphi-Omni-Sci is programmed to answer any Yes/No question about the physical world correctly by outputting Yes or No. It fails if asked if it is about to answer "No". .Close Paulson89 .Open Paulson89 James D Paulson Reasoning Tools to Support Systems Analysis and Design Ph. D Thesis UBC (Main library LE3 B7 1989 A1 P38) =THESIS TOOLS LOGIC SELMA ANALYSIS .See [SELMA] Summarized in .See [PaulsonWand92] Systems used Turbo Prolog and suffered from a combinatorial explosion, Need for Formal model at start and tools to enable error checking. .Close Pawlaketal95 .Open Pawlaketal95 Zdzislaw Pawlak & Jerzy Grymala-Busse & Roman Slowinski & Wojciech Ziarko Rough Sets Commun ACM V38n11(Nov 1995)pp89-95 =Theory AI LOGIC SETS summary: .See http://www/dick/maths/logic_31_Families_of_Sets.html#Bracketing sets .Close PeledGriesSchneider02 .Open PeledGriesSchneider02 Doron A Peled & David Gries & Fred B Schneider Software Reliability Methods Springer-Verlag NY Secausus NJ(2002) $69.95 ISBN 1852335173 CR 0303-0222 D.2.4 =TEXT FORMAL V&V SQA LOGIC LTL Buchi Hoare algebra Milner Petri sequence charts .Close PetersParnas00 .Open PetersParnas00 Dennis K Peters & David L Parnas Requirements-based Monitors for Real-Time Systems Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp77-85 =THEORY REQUIREMENTS LOGIC TEST TIMING ERRORS Mathematical specification of IN OUT REQ allow the derivation of a machine that observes IN OUT and reports if they are OK or not. could be used in testing an as safety device in use. In practice the monitor can fail. compare with user tests in XP! Compare with .See [Littlewood00] See [PetersParnas98] See [PetersParnas02] .Close Petre95 .Open Petre95 Marian Petre Why Looking isn't always seeing: Readership Skills and Graphical Programming Commun ACM V38n6(Jun 1995)pp33-44+letter V38n10(Oct 1995)pp19-20 =EXPERIMENT GRAPHIC LOGIC READABILITY expertise in domain makes a difference in strategy and outcome. flawed by use of bad graphic notations rather than good ones. Alternatively see .See [Scanlan89] .Close PettorossiProietti96 .Open PettorossiProietti96 Alberto Pettorossi & Maurizion Proietti Rules and Strategies for Transforming Functional and Logic Programs ACM Computing Surveys V28n2(Jun 1996)pp360-414 =Theory PERFORMANCE FUNCTIONAL LOGIC PROGRAMMING .Close PeytonJones86 .Open PeytonJones86 ?? Peyton & ?? Jones Parsing Distfix Operators Commun ACM 29 2 (Feb 1986) pp118-122 =DEMO DDD logic .Close PiccoRomanMcCann01 .Open PiccoRomanMcCann01 Gian Pietro Picco & Gruia-Catalin Roman & Peter J McCann Reasoning about code mobility with mobile UNITY ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp338-395 =THEORY FORMAL LOGIC UNITY MOBILE AGENT CODE .Close Pike06 .Open Pike06 Lee Pike A Note on the inconsistent axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-triggered Algorithms" IEEE Trans Software Engineering V32n5(May 2006)pp347-348 =CORRECTION LOGIC ERRORS TIMING PVS Refers to J. Rushby's paper in IEEE Trans Software Engineering V25n5(May 1999)pp651-660 Evidence that it is difficult to get axioms right, and that social processes correct and improve them... not tools and logic. The axioms model the behavior of clocks. The PVS tool was used to test for consistency by constructing a model that satisfies the new axioms. .Close Pittman93 .Open Pittman93 Matthew Pittman Lessons Learned in Managing Object-Oriented Development Special Theme "Making OO Work" IEEE Software V10n1(Jan 1993)pp43-53 =EXPERIENCE MANAGEMENT OBJECT-ORIENTED FSM ELH Page 48 Sidebar: Methods more alike than different. Two part approach. Part 1: candidate classes, attributes and behaviours, class structure, object structure, class design, process architecture, Reuse. Part 2(itterative) : Problem analysis, Domain Analysis, Architectural principles, Archictectural strategies, logical design, physical design Techniques that help Nouns and verbs, Checklists, Relationships: aggregation+claasification, Scenarios, responsibillities and colaborators, FSM & Statecharts, JSD ELHs for the protocols .Close PlatzerClarke08 .Open PlatzerClarke08 Andre Platzer & Edmund M Clarke Computing Differential Invariants of Hybrid Systems as Fixed Points CMU CS Technical Report .See http://reports-archive.adm.cs.cmu.edu/anon/anon/home/ftp/2008/CMU-CS-08-103.pdf (PDF) =MATHEMATICS MODEL LOGIC ODEs DIFERENTIAL EQUATIONS SAFETY HYBRID PROGRAMS Gives a way to compute whether formula describing important properties are true for all time or not. [\alpha]\phi = `all states reachable thru Hybrid program \alpha satisfy \phi`. Formulas assembled out of terms (expression ~ expression) for relation "~". Directional derivative of a term t wrt to vector equation D : x_dot = \theta, \nabla[t] = \nabla t.\theta. Differential Invariant of a formula F depends on \nabla[D]F is the conjunction of \nabla t.\theta over all terms `t` in F. .Close Popper59 .Open Popper59 Sir Karl Raymond Popper The Logic of Scientific Discovery Basic Books NY NY 1959 =THEORY SCIENCE POSITIVITISM Experiements can only prove a theory wrong. Good experiments should be designed to risk doing the unpredicted. .Close Quaglia08 .Open Quaglia08 Paola Quaglia On Beta-Binders Communications Montanari Festschrift pp456-472 .See [DeganoEtAl08] =IDEA MODEL BIOLOGICAL CELLULAR SYSTEMS CCS NON-SEQUENTIAL Instead of complementary paired actions (CCS) allows pairing of actions if they are of a compatible type. Defines syntax, equivalence, reductions, denotations, structural operational semantics,... Proves key results. .Close Racko95d .Open Racko95d Roland Racko Making the Miracle Happen Software Development Magazine(Oct 1995)pp93+99+101 =ESSAY adoption OBJECT-ORIENTED PROCESS STANDARDS IMPROVEMENT First improve your process, then adopt objects. .Box p93: "the first step is not to buy a C++ compiler or any other object-oriented language. If you are going to enter a rider into the multikilometer Tour de France bicycle race, you first need to make sure he is fit. " describes problems of average shop .Net |-(Racko95d_0): find out why - perhaps its best? |-(Racko95d_1): sell management on the bottom line benefits of improvement(not objects) |-(Racko95d_2): where does the overload come from: internal and/or external |-(Racko95d_2a): for external. sell "market directed optimization" or some such phrase to the management to handle it; wait for died down |-(Racko95d_3): training |-(Racko95d_3.1): walkthroughs and design concepts (coupling cohesion) |-(Racko95d_3.2): coders get together to hash out standards |-(Racko95d_3.3):a common vocab for words like: maintenance, good, design, walkthrough |-(Racko95d_4): teams develop goals, measurements and traceabillity methods |-(Racko95d_5): gather a stat base |-(Racko95d_6): The "market benefit phase" (objects). .Close.Net p101. How to handle a manager that shortens your estimates. (1) give a range of estimates: worst, best, most likely. Be ready to explain how best and worst cases can happen. (2) break out the time needed for integration. integration::= working design and code hierarchy so that the team can use them to connect the logic of the problem to real world, other systems, and physicla tchnology .Close.Box .Close RaghuRameshwhinston02 .Open RaghuRameshwhinston02 T S Raghu & R Ramesh & Andrew B whinston Representing Argumentation in Game Domains IEEE Computer Magazine V35n5(May 2002)pp68-70 =SIDEBAR FORMAL MODEL ACTON GAME DIALECTIC nonmonotonic LOGIC causality dialectic Gamma::=Net{fluents, actions, laws}. Fluents are time dependent propositions. Actions are made by players. Laws define the non-deterministic ways that actions change the fluents. .See http://www.cs.utexas.edu/users/v1/papers/nmct.ps Giunchiglia et al Apr 2002 Demo of how designers can discuss the implications of the laws and modify them using defeasible logic. .Close Ramsay88 .Open Ramsay88 Allan Ramsay Formal Methods for artificial intelligence Cambridge UP 1988 Q335.R35 ISBN 0-521-35236-3 =MONOGRAPH LOGIC AI FORMAL MODAL LPC TIMING NonMonotonic \lambda-calculus .Close RamseyFP60 .Open RamseyFP60 Frank Plumpton Ramsey (ed R B Braithwaite) Foundations of mathematics and other Logical Essays Littlefield Adams, Paterson NJ 1960 =ESSAYS PHILOSOPHY LOGIC MATHEMATICS TYPES PROBABILITY Essays, papers, reviews, and notes dating from the 1920s. .List Published .List The Foundations of Mathematics 1925 Mathematical Logic 1926 On a Problem of Formal Logic 1928 Note on the preceeding paper 1926 Facts and Propositions 1927 .Close.List Unpublished .List Truth and probability 1926 Further Considerations 1928 Last Papers 1928 .Close.List Appendix: Critical Notice of L Wittgenstein's "Tractatus Logico-Philosophicus" .Close.List PM::="Principia Mathematica", .See [WhiteheadRussell63]. Dispenses with PM's pphilosophical .Key axiom of reducibility by using Wittgenstein's `Tractatus Logico-Philosophicus`. .Box PM gives a syntactic definition set of special `predicative` truth functions to avoid paradoxes and then has to assume that all sets (for example) of objects of a given type can be expressed using one of these functions. Ramsey uses a semantic definition from Wittgenstein that makes any truth function `predicative`. .Close.Box Argues for the need for a theory of types. Does not discard axioms of infinity and selection. .Box PM's .Key Axiom of infinity asserts the existence of an infinite domain, Needed to define infinite numbers. Because, in PM, numbers measure the size of sets of objects of a particular type. Indeed a number is a set of all sets with the same size of that type. So the largest number for a given type is = to the size of the type. PM's .Key Axiom of selection is equivalent to the Axiom of Choice .See wikipedia .Close.Box .Close RaysideCampbell00 .Open RaysideCampbell00 Derek Rayside & Gerard T Cambell Aristotle and Object-Oriented Programming: Why Modern Students Need Traditional Logic ACM SIGCSE Bulletin V32n1(Mar 2000)pp237-244 (Proceeding of 31st SIGCSE Technical Symposium on C Sci Education Austion Texas) =SURVEY traditional LOGIC OBJECT-ORIENTED traditional logic is about meaning rather than formal manipulation of symbols. Meaning defined by a heirarchy of general and specific classification. Doesn't distinguish between behavioural and structural properties. .Close Reichenbach47 .Open Reichenbach47 Hans Reichenbach Elements of Symbolic Logic The Macmillan Co., NY NY. 1947 5th edition 1956 BC 135 R4 =THEORY LOGIC LANGUAGE PHILOSOPHY This book is most famous for analyzing all the tenses found in most natural languages .See ./samples/tenses.html in terms of three times: S=time of Speech, R=a time Referred to, and E=time(s) when Event occurred(was occurring). For example "It was raining in Manchester in 1935" has S="August 2006", R is some time in 1935, and E is a range of times surrounding R when it was raining. If "I will see you tomorrow" is spoken on day S, then it's R is the day after S and E is a time in that day. Reichenbach argues that all three times: E,R and S are needed to explain all the tenses. He also shows that R tends to be the same inside a sentence except where it is explicitly shifted. This tends to be true across sentences as well.... except that later authors give many counter examples where the times interact with the link: narrative, explanation, elaboration, etc. holding between the sentences. The book is a thorough and persnickety philosophical analysis of natural language and thought in terms of symbolic logic. It harks back to Whitehead and Russell's `magnum opus` .See [WhiteheadRussell63]. It has an excellent list .See ./samples/tautologies.html of `true` formulas. .Close Ressler93 .Open Ressler93 Sandy Ressler Perspective on Electronic Publishing: Standards & Solutions and more Prentice Hall Englewood Cliffs NJ 1993, ISBN 0-13-287491-1 .See [CR] 9407-0424 =TEXT WWW/NET DOCUMENTS .Box Review ch1 views: visual, logical, design(fonts,...), communications(pragmatics), engineered, database ch2 Form and function ch3 Document standards SGML ODA de Facto ch4 Graphics and integration ch5 Choice ch6 management ch7 case studies Not enough detail, for novices, good questions, few answers .Close.Box .Close Roberts73 .Open Roberts73 Don D. Roberts The Existential Graphs of Charles S. Peirce The Hague 1973 Mouton B945.P44 R6 =ADVERT GRAPHIC LOGIC .Close RobertsonAgusti99 .Open RobertsonAgusti99 David Robertson & Jaume Agusti Software Blueprints: Lightweight Uses of Logic in Conceptual Modeling Addison Wesley ACM Press NY NY 1999 Order# 704992 ISBN 0-201-38919-2 .See [CR] 0001-0008 =MONOGRAPH LOGIC Prolog MODELS ANALYSIS DESIGN PROOFS BSDM SIMULATION SKELETONS Argumentation Temporal SYNTAX SEMANTICS network:= Net{ R:=requirements:Sets, P:=Positions:Ssets, issues:Sets, D: decisions:Sets, specialize:@(R, R), generate:@(R, I), adopted_in_response_to:@(P, I), suggest:@( I, P), based_on:@(D, P), resolve:@(D, I), depend_on:@(D, D) }. .See [RameshLuqi93] (dick)|- `Use Prolog notation. Solutions assume perfect typing!`. abduction, induction, deduction. defeasible logics. can_not_be_shown ( P ). argumentation. endorsement. Systems dynamics models - (dick)|- `inadequate numerical method` BSDM ::=`Existence dependency model`. Example: maintaining www pages! .Close RobinsonjPurao09 .Open RobinsonjPurao09 William N Robinson & Sandeep Purao Specifications and Monitoring Interactions and commitments in Open Business Processes IEEE Software Magazine V26n2(Mar/Apr 2009)pp72-79 =IDEA SERVICE BUSINESS PROCESS MODEL UML SEQUENCE DIAGRAMS OCL TEMPORAL LOGIC REQUIREMENTS MONITORING When many different components and/or actors provide services to each other ... with the network being dynamically configured, one must define the interactions precisely and monitor to see if they are being followed. For example, after a bill is sent to a customer, one expects to be paid... UML Sequence charts can show the protocols: patterns of messages. Add to this .Key conditional commitments (CC) with four parts .List The actor who is committed to bring something about: customer. The actor who expects the the commitment: biller. The statement that becomes true: customer send payment. The conditions under which it becomes true: the biller billed the customer. .Close.List Proposes a temporal logic extension to the OCL with clause like "after time until time...", "always....", "never ...", "eventually ...", By using existing logging service we can monitor the interactions and collect information on how well commitments are being kept. Then see .See [RobinsonWN10] .Close RobinsonWN10 .Open RobinsonWN10 William N Robinson A roadmap for comprehensive requirements monitoring IEEE Computer Magazine V43n5(May 2010)pp64-72 =IDEAS MONITORING REQUIREMENTS COMPLEX SYSTEMS BAM FEEDBACK OCL TEMPORAL LOGIC Overly complex attempt at a universal theory of monitoring systems to see if they are fulfilling requirements. BAM::="business activity monitoring". Model user requirements and compare with the streams of the events that occur. Based on .See [RobinsonjPurao09] .Close Roetzheim00 .Open Roetzheim00 William Roetzheim Estimating Software Costs Software Development Magazine V8n9(Oct 2000)pp66-68 =TUTORIAL COCOMO COSTS KSLOC Effort: PersonMonths = a* KSLOC^p, where a & p depend on project. a in 2.5..3.60, p in 1..1.2. SLOC by sum of module estimates using mean = ( bet + worst + 4*expected)/6, sd =( worst - best )/6 or by function points (fp) based on number of inputs*4 + files*7 + outputs*5 + queries*4 + logical database tables*10. sloc = c * fp, c depends on the language. .Close Rosen00 .Open Rosen00 Keneth H Rosen(editor in chief) Handbook of discrete and combinatorial mathematics CRC Press Dnvers NY 2000 ISBN 0-8493-0149-1 QA164.H36 1999 =REFERENCE LOGIC DISCRETE MATHEMATICS ALGORITHMS GRAPHS .Close Rushby97a .Open Rushby97a John Rushby Subtypes for Specifications in .See [JazayeriSchauer97] pp4-19 =EXPERIECE LOGIC PREDICATES TYPES useful to use predicate to define subtypes an use subtypes in quantifiers etc in logic in specifications+proofs+assertions+functions Tool = .See [PVS] Also see .See [RushbyOwreShankar98] .Close RushbyHenke92 .Open RushbyHenke92 John Rushby & Friedrich von Henke Formal Verification of Algorithms for Critical Systems ACM SIGSOFT'91 Conf on Software for Critical Systems: Software Eng Notes V16n5(Dec 1991)pp1-15, republished IEEE Trans SE-19n1(Jan 1993)pp13-23 =EXPERIENCE PROOF CHECKER LOGIC EHDM Z EHDM - the "implacable sceptic" .Box need for a proof checker with library of reusable theories including both discrete and concrete mathematics - the "implacable sceptic" forcing you to express all assumptions, found errors in published work, typos in Z specification, corrected and simplified publishable proof of a complex real time algorithm, able to rapidly do 'what ifs', productive symbiosis, tools: editor, parser, typechecker, browesers, cross-referenceers,...typographical output, a sort of module structure for specifications, first order logic with a fragment of higher order logic (functions of functions), 19 axioms and 200 proofs ICA problem as a challenge Need reusable library of theories Need a type theory which distinguishes similar algebras like velocity vs length or real time vs clock time. .Close.Box .Close RushbyOwreShankar98 .Open RushbyOwreShankar98 John Rushby & Sam Owre & Natarajan Shankar Subtypes for Specifications: Predicate Subtyping in PVS IEEE Trans SE V24n9(Sep 1998)pp709-720 =THEORY LOGIC partial .See [PVS] Also see .See [Rushby97a] Compare .See [Parnas93] .Close SaariluomaIsomki08 .Open SaariluomaIsomki08 P Saariluoma & H Isomki Future interaction design ii (1st ed.) Springer Publishing Company, Incorporated, 2008 $CR 1003-0249 =THEORY =EXPERIMENT =SURVEY PHILOSPHY USER HCI SOCIOLOGY GERONTECHNOLOGY ANTHROPOLOGY Intro+9 papers .List Need to replace folak lore by science. Gerontechnology Virtual vs real -- 3 experiments Need to combine technological and psychological models. Monitor cognitive load and modify. partial history of scientific psychology in design. History of HCI experiments. Mobile devices must be tested outside. SUX::="service user experience". locative media. Urban. Actor-network theory ANT constructivist. technology acceptance vs appropriation purpose and meaning continuously redefined by users. Anthopology. need holistic view of human. Modes of being. Phenomenology. Metatriangulation. .Close.List No ref to .See [Dwyer81] ! .Close Sain92 .Open Sain92 Ildiko Sain Temporal Logics and their Clocks Theor Comput Sci V95n1(Mar 23 1992)pp75-95 CR9303-0168(M Abadi) =Theory Logic Concurrent .Close Schaefer06 .Open Schaefer06 Robert Schaefer A Rational theory of System-making systems ACM SIGSOFT Software Engineering Notes V31n2(Mar 2006)p31 (online supplement pp1-20) =ESSAY LARGE SYSTEMS FAILURE DILBERT =SURVEY SOCIOTECHNICAL PEOPLE POWER PLANS PROGRAMS PROCESSES POLITICS BUREAUCRACY Large projects/systems tend to fail for complex endemic sociological reasons. A key problem: separating the planner/designer/thinker from the doer. The plan/design can not handle all the contingency and the doer is forbidden to be creative when handling the unexpected. For more see .See [Dumay06] on BPR in conflict with people. .Close Schaefer07 .Open Schaefer07 Robert Schaefer The Grand Theory of Everything: What Man-Made Systems are, and Why They Fail ACM SIGSOFT Software Engineering notes V32n4(Jul 2007)p31 .See http://doi.acm.org/10.1145/1281421.1281430 (links to a 26 page PDF) =JOKE? THEORY FAILURE tGToE tGToE::="the Grand Theory of Everything". Written in an 18th century Style -- with Many `definitions` and Random Capitalizations but Getting Close to Heart of the Reason for Complex Systems Failing. Here is a Cogent Quotation from the Verbose and Jocular Paper: .Box In the practice of Systems Development, Rules are enumerated to comprise a Finite sized Set of Constraints. This Set in Systems Development is called the Requirements (in Systems Use these are called Policies). The number of Freedoms that a System has is the Inverse of that Finite Set of Constraints which by Rules of Logic are Infinite in number. This relationship of Finite Rules and Infinite Freedoms is more than a Curiosity, as in the mapping of a Solution into a Model of Behavior, the Rules become Contractual Shalls (A "Shall" being a Statement that Indicates a Contractual Obligation of Legal Consequence) while the Inverse, Freedoms, become the Infinite Set of "Shall Nots. That Infinite Set of Shall Not Behaviors represents a Set which can never be Fully Imagined, and thus can never Fully Defined, Implemented, or Tested. Because this Set can never be Fully Defined it is customarily Replaced with a Time and Money based Stopping Criteria, i.e. to Proceed along the set of Requirements (that One hopes is at least a "well-defined" Subset of Infinity) until the Requirements are Implemented and Tested, or the Customer's Will as measured by Time and Money, Runs Out. Note that at this Stopping Point there may be a Gap between "What Is", and "What Is Desired". In terms of Systems Reliability, this Gap is called a Hazard. .Close.Box To summarize: requirements are always incomplete and some conditions will always be untested. Also see .See [Schaefer06] and .See [Gall79]. .Close SchiederBroy99 .Open SchiederBroy99 Birgit Schieder & Manfred Broy Adapting calculatonal logic to the Undefined Computer Journal V42n2( 1999)pp73-81 =THEORY LOGIC MATHEMATICS FORMAL Dijkstra, Gries, no ref to .See [Parnas93] Shows three value: true, false and undefined calculus which allows recursive definitions via a Fixed point rule of inference. .Close SchneiderK04 .Open SchneiderK04 Klaus Schneider Verification of Reactive Systems: Formal Methods and Algorithms Springer-Verlag London UK 2004 ISBN 3540002960 $CR 0409-1013 =THEORY FORMAL V&V ALGORITHMS MODEL CHECKING Borel FIXPOINT AUTOMATA MODAL LOGIC .Close SchnuppBernhard87 .Open SchnuppBernhard87 Petter(?) Schnupp & Lawrence W. Bernhard Productive Prolog Programming Carl Hanser Verlag and Prentice Hall International(UK) 1987 =HOWTO PROLOG logic-programming DDD JSP Reality .Close Schock69 .Open Schock69 R Schock Logics without Existence Assumptions Almqvist & Wikells 1968 Stockholm Sweden =THEORY FORMAL LOGIC See .See [LPT] and .See [LPV] .Close Scott76 .Open Scott76 Dana S Scott Logic and Programming Languages Turing Award Lecture 1976 .See [ACM86] =AUTOBIOGRAPHY =MATHEMATICS INTRODUCTION SCOTT FUNCTION SPACES LATTICES POSETS SEMANTICS Provides a semantics for typeless \lambda calculus. .Close Selic00 .Open Selic00 Bran Selic A generic framework for modeling resources with UML IEEE Computer Magazine V33n6(Jun 2000)pp64-69 =MODEL QoS OMG UML PERFORMANCE MODEL distinguish logical model from the engineering (physical) model. .Close Shanahan97 .Open Shanahan97 Murray Shanahan Solving the Frame Problem: A Mathematical Investigation of the common sense law of inertia MIT Press Cambridge MA 1997 ISBN 0-262-29384 .See [CR] 9802-005 =THESIS AI LOGIC FRAMES INERTIA .Close Shankar93 .Open Shankar93 A Udaya Shankar An Introduction to Assertional Reasoning for Concurrent Systems ACM Computer Surveys V24n3(Sep 1993)pp225-262 =Tutorial concurrency fairness safety non-sequential temporal logic Prereq for LamShankar94 & Jonsson94... refers to Lamport, UNITY, Mana et al .Close ShankarAsa03 .Open ShankarAsa03 Subash Shankar & Sinan Asa Formal Semantics of UML with Real-Time Constructs LNCS 2863 <<UML>> 2003 -- The Unified Modeling Language Oct 2003, pp60-75 =THEORY SEMANTICS TIMING UML SEQUENCE STATECHARTS TEMPORAL LOGIC PTL .Close Shao10 .Open Shao10 Zhong Shao Certified Software Commun ACM V53n12(Dec 2010)pp56-66 .See http://doi.acm.org/10.1145/1859204.1859226 =IDEAS DEPENDABLE CORRECT PROOF CHECKER ASSEMBLER MACHINE CODE TOOLS EXAMPLES Coq METALOGIC FUNCTIONAL NONSEQUENTIAL Minimize the components that can damage the dependability of the system. Both proofs and specifications can be represented by executable programs. Example using CoQ (Wikipedia)|- Coq implements a dependently typed functional programming language... .See en.wikipedia.org/wiki/Coq "huge cost in constructing ... specifications and proofs" Dynamic validation - add a check after an unproved step and use a proved component if the check fails. "time to market is likely terrible" PCC - proof-carrying code - give executable code with a proof of safety to a host that checks the proof. Proof checking is automated and about as difficult as type checking. FPCC - Foundational PCC. CAP - certified assembly programming - using a mechanisable Metalogic. Modular reasoning. Separation logics. CSL - concurrent separation logic. Domain specific logics. There exist certified garbage collectors, thread libraries, compilers, and certifying compilers, etc. (dick)|-How to handle changing requirements and specifications? Can proofs be agile? .Close Shin95 .Open Shin95 Sun-Joo Shin The Logical Status of Diagrams Cambridge U Press UK 1995 $39.95 197+pages =THEORY GRAPHIC LOGICS .Close SiddiqiShekaran96 .Open SiddiqiShekaran96 Jawed Siddiqi(Sheffield Hallam U UK) & M Chandra Shekaran(MS) Requirements Engineering: The Emerging Wisdom IEEE Software magazine V13n3(Mar 1996)pp15-19 =EDITORIAL REQUIREMENTS ENGINEERING introduction to special theme articles pp20-64 RE::=systems analysis with engineering orientation effect of context+need to handle changing context+questioning what.vs.how and the functional.vs.nonfunctional + problem frames and repetoire of methods( Jackson95)+anthopological approach + non-contractual forms of requirements(no one-size) .Close SiffReps99 .Open SiffReps99 Michael Siff & Thomas Reps Identifying Modules via Concept Analysis IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp749-768 =THEORY =DEMO EVOLUTION MODULES C to C++ LOGIC TOOL Improves on Snelting's work .See [Snelting96] .See [SneltingTip98] Use function vs struct attributes. Concept partition:=modules where each function linkd to one module. may need to add attributes. include negative information. Tested on SPEC 95 benchmark, case studies on chull and bash .Close SmithA90 .Open SmithA90 Alf Smith The Knuth-Bendix Completion Algorithm and its Specification in Z pp195-220 in .See [Nicholls90] =DEMO SPECIFICATION Z Mathematics vs Logic cf .See [NelsonOppen80] .Close SobelClarkson02 .Open SobelClarkson02 Ann E Kelley Sobel & Michael R Clarkson Formal methods application: An Empirical Tale of Software Development IEEE Trans Software Engineering V28n3(Mar 2002)pp308-320 + Correspondence (Beery & Tichy) V29n6(Jun 2003)pp567-575 =EXPERIMENT FORMAL NONSEQUENTIAL LOGIC SPECIFICATION DERIVATION METRICS UML lift problem c++ MFC Compared formally vs informally developed programs by students for controlling elevators.nn E Kelley Sobel & Michael R Clarkson Formal methods application: An Empirical Tale of Software Development IEEE Trans Software Engineering V28n3(Mar 2002)pp308-320 + Correspondence (Beery & Tichy) V29n6(Jun 2003)pp567-575 =EXPERIMENT FORMAL NONSEQUENTIAL LOGIC SPECIFICATION DERIVATION METRICS UML lift problem c++ MFC Methods first order logic, UML diagrams,pseudocode, differences: formal group 100% functional vs <50% of the informal groups. most formal groups handed in UML vs no informal groups did. Similarities. No statistically significant difference in conciseness and complexity of code, Includes a formal solution of one algorithm developed after the experiment by some of the students. Daniel M Berry & Walter F Tichy wrote following, .Net Glad that somebody did some empirical research. Self selected groups weaken result. Hawthorne and Novelty also weaken result. No knowledge of what happened in "control" groups. Correctness results based on very few test cases. No discussion of external threats to validity. Sobel & Clarkson replied following, .Net Educational research (teaching formal methods) is not an industrial or lab experiement. .Close.Net .Close.Net .Close SotirovskiKruchten95 .Open SotirovskiKruchten95 Drasko M Sotirovski & Phillipe B Kruchten Implementing Dialogue Independence IEEE Software Magazine(Nov 1995)pp61-70 =DEMO MODULES ARCHITECTURE PATTERNS HCI USER HIDE LOGIC separation of user interface and core application by using glue objects for existence properties and transitions `glue` is like a two-way version of the Observer pattern. Compare with class type architecture and many others .Close SowmyaRamash98 .Open SowmyaRamash98 Arcot Sowmya & S Ramash Extending Statecharts with Temporal Logic IEEE Trans SE V24n3(Mar 1998)pp216-231 =DEMO DYNAMICS STATECHARTS TEMPOAL MODAL LOGIC FNLOG::="Logic-Based Function Specification Language". .Close Spivey89 .Open Spivey89 J Michael Spivey The Z Notation: A reference Manual Prentice Hall Series in C Sci 1989(UK) =handbook formal logic Later see .See [Spivey01] (online) .Close Spivey92 .Open Spivey92 J Michael Spivey The Z Notation: A Reference Manual Prentice Hall Series in C Sci 1992(UK) ISBN 0-13-978529-9 CR 9307-0424(D.2.1) =handbook formal logic Earlier was .See [Spivey89] later on the web .See [Spivey01] as PDF. .Close Spivey01 .Open Spivey01 J M Spivey The Z Notation: A Reference Manual (online) Web 2001 .See ./samples/zrm.pdf .See http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf =handbook formal logic Z SPECIFICATION Earlier citations/versions .See [Spivey89] .See [Spivey92] .Box Quote from web site .See http://spivey.oriel.ox.ac.uk/mike/zrm/index.html The Z Reference Manual has now been allowed to go out of print by the publisher, Prentice Hall, but they have kindly returned the copyright to me, so I can make the full text available here. Please note that I have not placed the copyright of this work in the public domain. Nevertheless, I freely grant permission to make copies of the whole work for any purpose except direct commercial gain. I retain all other rights, including but not limited to the right to make translations and derivative works, and the right to make extracts and copies of parts of the work. Fair quotation is permitted according to usual scholarly conventions. .Close.Box .Close SpohrerRiecken06 .Open SpohrerRiecken06 Jim Spohrer & Doug Riecken (Eds) Service Science (Special Issue/Section) Commun ACM V49n7(Jul 2006)pp30-87 =SURVEY =ADVERT RESEARCH CONSULTANCY SERVICE INDUSTRY ECONOMICS SSME 3S WEB2.0 CRM Introduction + 12 articles/papers p33: 55 references. If you divide the economy in agriculture, manufacture, and service then most of it is now service! Even when selling product, service can make the difference. This change means that research and education needs to develop (or at least) shift to a focus on service rather than production. SSME::="Services Science, Management, and Engineering". Service implies: .Box Expertise and knowledge by the supplier. But the suppliers knowledge must be fitted to customers specific environment. Services are a socio-technical system and not a pure technological fix. Need to model/understand the people and organization of the customer. Exchange of service for something of value. Negotiation, interaction, and trust between customer and supplier. Long term relations with customers. Communication is vital. Service often encoded as software+hardware --algorithmic. 3S:="An ontology describing services: humans, web, software, ..." Innovation and perhaps revolution in the enterprise. New courses and schools. .Close.Box (dick)|- with luck they will rediscover systems analysis and operations research from the 1950s. .Close StepanovMcJones09 .Open StepanovMcJones09 Alexander Stepanov & Paul McJones Elements of Programming Addison-Wesley Professional (June 09, 2009) Print ISBN: 0-321-63537-X Web ISBN 0-321-64392-5 Safari $CR 1105-0457 .See http://www.elementsofprogramming.com/book.html =TEXT THEORY C++ PROGRAMMING FORMAL LOGIC MATHEMATICS ALGORITHMIC CODE GENERIC ABSTRACTION ADT .Close Stephenson07 .Open Stephenson07 Peter Stephenson AMenaza SecuriTree has a different view of Risk Analysis CS Magazine for Security Professionals, (Feb 2007)p67 =REVIEW TOOL Fault trees LOGIC SECURITY REQUIREMENTS RISK ANALYSIS Amenaza SecuriTree See .See http://www.amenaza.com .Close Stevens95 .Open Stevens95 Anthony Stevens Review of "Information Modeling: Specification and Implementation" (Edmond92) Comp Rev V36n1(Jan 1995)p62 .See [CR] 9501-0017 =REVIEW REFINEMENT Z SQL "[...]impression that SQL had become integrated with[...]Z What unifies the two fields are the basic concepts of discrete mathematics - sets, relations, functions, and logic. [...] training materials for a systems nalysis courses with a modern flavore[..]well-thought-out and extensive examples[...] humor[...]" "[Refinement...] it appears that this part of formal methods continues to be a kind of mental torture. When we specify formally, we seem to say so much with so little, whereas when we refine, we seem to achieve so little with so much." .Close StrawsonOderberg05 .Open StrawsonOderberg05 P Strawson & David S Oderberg Eds. The old new logic: Essays on the philosophy of Fred Sommers MIT Press Cambridge MA ISBN 0262151138 CR 0710-0977 =UNREAD Aristotle Syllogism TERMS TLP vs MPL PREDICATE TLP::="Term Functor Logic". Instead of predicates, facts are expressed in terms like [-S+C]+[W+S]-[W+C]. Simplifies many arguments that are complex in LPC. .Close StubblebineWright02 .Open StubblebineWright02 Stuart G Stubblebine & Rebecca N Wright An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency IEEE Trans Software Engineering V28n3(Mar 2002)pp256-285 =THEORY LOGIC TEMPORAL BELIEF DISTRIBUTED TIME PROTOCOLS BAN web certificates Kerberos5 .Close Sutton00 .Open Sutton00 Stanley M Sutton Jr. The Role on processes in a Software start-up IEEE Software Magazine V17n3(Jul/Aug 2000)pp33-39 =ESSAY EXPERIENCE ECCubed ORGANIZATION PROCESS if startup then inexperienced and lmited resources and multiple changing constraints and changing technologies and need speed and small. Define but remain flexible using suitable techniques for most useful subprocesses. Generalize. generic procedures and technological infrastructure. Learn from experiences. Only define reusable procedures. Hire competent techical people and superstar managers. .Close Tayloretal96 .Open Tayloretal96 Richard N Taylor & Nenad Medvidovic & Kenneth M Anderson & E James Whitehead Jr. & Jason E Robbins & Kari A Nies & Peyman Oreizy & Deborrah L Dubrow A Component- and message- based Architectural Style for Gui Software IEEE Trans Softw Eng VSE22N6(Jun 1996)pp390-406 revised from ICSE-17 1995 =DEMO Chiron2/C2 decomposition ARCHITECTURE COMPONENT MESSAGE NONSEQUENTIAL MODULES Compare with .See [RajlichSilva96] layered modules of two types: components and connectors. decoupling: Connector<->component<->connector... message::= request|notification. layers(like onion with logical ADTs in center). requests flow in and notifications out. Notifications are not necesarily acted on. .Close Terwilliger93b .Open Terwilliger93b Robert W Terwilliger <terwilli@cs.colorado.edu> An Example of Process Verification: the Gries/Dijkstra Design Process ACM SIGSOFT Software Engineering Notes V18n3(Jul 1993)ppA26-35 =CASE-STUDY V&V CORRECTNESS FORMAL LOGIC DESIGN PROOF .Close ThimblebyLadkin96 .Open ThimblebyLadkin96 Harold Thimbleby & Peter Ladkin From logic to manuals .See http://www.cs.mdx.ac.uk/Harold/papers/log2manop.html =DEMO TOOL LOGIC LANGUAGE TABULAR DOCUMENTATION WWW Manuals Shows how to prepare manuals with boolean expressions that are automatically, indexed, linked, and converted into tables. .See http://www/dick/notes/ThimblebyLadkin96.html .Close ThimblebyLadkin97 .Open ThimblebyLadkin97 H. W. Thimbleby & P. B. Ladkin From Logic to Manuals Again IEE Proceedings Software Engineering, 144(3),pp185-192, 1997 =DEMO LOGIC DOCUMENTATION TLA FSM/STD HCI Compare .See [ThimblebyLadkin96] .Close Thomas90 .Open Thomas90 Automata on Infinite Objects in .See [Leeuwen90] pp133-187 =THEORY MODEL MODAL LOGIC TEMPORAL Buchi AUTOMATA FSM/STD .Close Tillman93 .Open Tillman93 George Tillman A Practical Guide to Logical Data Modelling McGraw-Hill Inc New York NY 1993 ISBN 0-07-064615-5 CR9411-0772 .Close Toulmin58 .Open Toulmin58 Stephen Edelston Toulmin The uses of argument. Cambridge [Eng.] University Press, 1958 BC177 =THEORY INFORMAL LOGIC ARGUMENT RATIONALE Developed into text .See [ToulminRiekeJanik78] .Close ToulminRiekeJanik78 .Open ToulminRiekeJanik78 Stephen E Toulmin & Richard Rieke & Allan Janik An introduction to reasoning Macmillan, c1979. New York BC177 .T59 =TEXT INFORMAL LOGIC ARGUMENT RATIONALE GRAPHIC Based on .See [Toulmin58] Toulmin_argument::=data "--->" O(qualifier) claim ", " warrant O(backing) O(rebuttal) . .As_is Backing .As_is | .As_is Warrant .As_is | .As_is Data -------------> (Qualifier) Claim .As_is | .As_is Rebuttal Toulmin_argument::=following .Net Claim::Utterance, conclusions Data::Utterance, facts Warrant::Utterance, general rule linking the data to the claim. Backing::Utterance, credentials when the warrant is not convincing enough. Rebuttal::Utterance, restrictions which apply to the claim. Qualifier::Phrase, possibly, likely, probably, certainly, presumably, necessarily. .Close.Net .But .See [Loui08] .See [HaleyLaneyMoffettNuseibeh08] .Close.But .Close Tremblay99 .Open Tremblay99 Guy Tremblay Exercises for Teaching Logic in a Formal Methods Course: Formalizing ERDs ACM SIGCSE Bulletin -- Inroads V31n1(Mar 1999)pp100-104 =DEMO Spec .Close TsaiWiegertJang92 .Open TsaiWiegertJang92 Jeffrey J P Tsai & Thomas Weigert & Hung-chin Jang A Hybrid Knowledge Representation as a Basis of Requirement Specification and Specification Analysis IEEE Trans SE-V19n12(Dec 1992)pp1076-1100A =SUVEY FRORL LOGIC FORMAL SPECIFICATION OBJECT-ORIENTED non-monotonic hierarchy .Box ORIENTED non-monotonic hierarchy(general with exceptions) frames for objects and activities complete and sound. Compare Kaindl93 arguing for frames to support informal preparations. Section I Introduction(pp1076-1077) p1076: "Software development usually begins with an attempt to recognize and understand the user's requirements[...] Software developers are always forced to make assumptions about the user's requirements[...] Often the user has an incomplete understanding[...]" Goguen and Meseguer's work on FOOP 1987 (Functions+objects+relational methods) p1077: "an_instance_of", "a_kind_of", "a_part_of". "formal correctness checking is desirable[...]surpass the expressiveness of standard first order logic"... "complete and sound with respect to these semantics[Horn clause logic+nonmonotonicity]. [...] the users can automatically analyze various properties of a FRORL specification." Section II Demands(pp1077-1078) p1077 "domain model[vs]specification" "theorems [---] facts" Section III The language(pp1078-1081) p1078 "Given an informal description of the problem domain" operational and decalrtive interpretations possible. p1079 Refers to Booch91 and Kowalski's book Section IV Semantic foundations(pp1081-1085) Predicates and Consistency (\para_symbol) statements, Horne clauses, Herbarnd interpretations, fixed points of a theory operator. some model theoretic semantics. Some computational procedure to indicate if a clause is a logical consequence of a theory Section V Mapping FRORL into Semantics(pp-) Section V Analysis of specifications(pp1085-1090) reachability, reversibillity, liveness, and consistency. State space or problem reduction. Use abstracted attributes. Section VII Software Environment(pp1090-1093) Sun SparcStation Open Look Section VIII Related work (pp1093-1096) Survey based on Wing88. Mentions with KATE, CAKE, LARCH, Ina Jo, GIST, SASCO, PLEASE, SXL,... Section IX Conclusions and plans(pp1096) Section X. Appendix BNF(pp1096-1097) Section XI Appendix B Soundness and Completeness (pp1097-1099) 54 References (pp1099-1100) .Close.Box .Close TuckerNoonan02 .Open TuckerNoonan02 Allen B Tucker & Robert E Noonan Integrating Formal Models into the Programming Language Course SIGCSE'02 Proceeding & ACM SIGCSE Bulletin V34n1(Mar 2002)pp346-350 =EXAMPLE FORMAL SPECIFICATION J denotational semantics implemented with objects(Java), functions(Scheme), and logic(Prolog) Note. the OO implementation is like Botting99 .Close Turpin93 .Open Turpin93 Russell Turpin<turpin@cs.utexas.edu> A logical Approach to Data Structures In .See [Notkin93] pp138-148 =THEORY DATA STRUCTURES PROOF POINTERS .Box Part of Texas Adv Res Proj, admin J C Browne. Formal development and verification of data structure programs. pointers and destructive update. "well known to programmers but they are usually informally defined by the programming community or operationally defined in particular imperative languages" NO!: implementations. Concepts: data structures address, pointer reference, data structure disjointness, data structure isomorphism. "gap between the formalisim that was provided and the way in which the problem area is naturally discussed... common textx on formal verification omit pointers from their prescription for programming. Predicates PartOf(x,y), Dangles(p,x) ::=`p is not NULL but x has no part with address p`, HasDangles(x), Navigable(x), Disjoint(y,x), y":"":"x Status: prototype compiler, graphical interface, mapping to standard theprem prover, incomplete....environment enforces a greater attention to invariants, details, and exceptional conditions. Debugging moved to compile time. out-of-bounds suscripts and mangled pointers are eliminated. records See [1] Beeri Catriel et al "Embedding \Psi- terms in a Horn-clause Logic Language" MCC Tech Report ACA-ST-050-88. objects See [12] MaierD86, "A Logic for Objects" In Proc o t Workshop on the Foundations of Deductive Databases and Logic Programming, Washington DC, Aug 1986 pp6-26. Galois programs specified in logic: name, modes for arguments, goal predicate, precondition - no unification or clausal search required. Composition generates proof obligations: Prerequisite asssertion .Close.Box .Close TyszberowiczYehudai92 .Open TyszberowiczYehudai92 Shmuel Tyszberowicz & Amiram Yehudai OBSERV -- A Prototyping Language and Environment ACM Trans Softw Eng Methodol V1n3( Jul 1992 )pp 269-309 =THEORY RAD GRAPHIC OBJECTS CONCURRENCY LOGIC PROGRAMMING STDs/FSMs - no backend .Close Vadaparty06 .Open Vadaparty06 Sirisha Vadaparty Semantic Tableaux Program CSUSB CSci Master Project 2006 .See http://csci.csusb.edu/dick/seminar/20060222SirishaVardaparty.txt =DEMO LOGIC PROOF TOOL TREE CASES LPC Java .Close vanBenthem97 .Open vanBenthem97 Johan van Bentham Exploring Logical Dynamics Center for Study of Lang and Info Stanford CA 1997 ISBN 1-57586-059-7 $59.95 CR9712-0979 =MATHEMATICS LOGIC RELATIONS DYNAMICS .Close Venture78 .Open Venture78 Alec Venture Loglan -- a more flexible language =LETTER Esperanto vs Loglan Volapuk LOGIC ITL UNIVERSAL LANGUAGES Computer Weekly (UK) (Mar 23 1978)p19 Rebuts Taylor78 and Botting78a. .Close VesseyWeber86 .Open VesseyWeber86 Iris Vessey & Ron Weber Structured Tools and Conditional Logic: An Empirical Investigation Commun ACM V29n1(Jan 1986)pp48-57 =EMPIRICAL STRUCTURED SEQUENTAL SP LOGIC GRAPHICS different representations for different purposes overall superiority of decision trees vs linear sequence of program language text compare .See [Petre95] .Close WangBastaniYen05 .Open WangBastaniYen05 Dongfeng Wang & Farokh B Bastani & I.-Ling Yen Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance IEEE Trans Software Engineering V31n9(Sep 2005)pp713-732 =IDEA MATHEMATICS MODAL LOGIC TLA ASPECTS COMPONENTS NONDETERMINISTIC FSM RHSM IDEAL BART .Close WandWeber90 .Open WandWeber90 Yair Wand & Ron Weber An Ontological Model of an Information System IEEE Trans SE-16n1(Nov 1990)pp1282-1291 =THEORY SYSTEM Formal Mathematics Systems decomposition .Close WangBastaniYen05 .Open WangBastaniYen05 Dongfeng Wang & Farokh B Bastani & I.-Ling Yen Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance IEEE Trans Software Engineering V31n9(Sep 2005)pp713-732 =IDEA MATHEMATICS MODAL LOGIC TLA ASPECTS COMPONENTS NONDETERMINISTIC FSM RHSM IDEAL BART .Close WardM96 .Open WardM96 Martin Ward Derivation of Data Intensive Algorithms by Formal Transformation: The Schnorr-Waite Graph Marking Algorithm IEEE Trans SE V22n9(Sep 1996)pp663-686 =THEORY LOGIC SPECIFICATION DERIVATION ALGORITHM DATA action language with specification statements steps introduce ghost variables steps can combine data structures that both drive and are developed by the algorithms .Close Warnier76 .Open Warnier76 Jean Dominique Warnier The Logical Construction of Programs Out of print. see pp 85-105 of ParikhZvegintzov82 =HANDBOOK =CLASSIC TECHNICAL DESIGN LCP DDD Bracketted notation. Data structures first, then operations, then place ops in data. Source for the Warnie-Orr methods. Compare JSP. .Close Warnier81 .Open Warnier81 Jean Dominique Warnier Logical Construction of Systems Van Nostrand Reinhold NY NY 1981 =SURVEY LCS data Follows .See [Warnier76]. .Close WeberWeisbrod03 .Open WeberWeisbrod03 Mathias Weber & Joachim Weisbrod Requirements Engineering in Automotive Development: Experiences and Challenges IEEE Software Magazine V20n1(Jan/Feb 2003)pp16-24 =EXPERIENCE REQUIREMENTS TOOLS PROCESS DaimlerChrysler tools .List DOORS::="Dynamic Object Oriented Requirements System", .See http://www.telelogic.com/Products/doors/doors/index.cfm (was Telelogic, now IBM). RequisitePro::=http://www.rational.com/products/reqpro. RTM::="Requirements Traceability and Management", .See http://www.chipware.com/ .Close.List Complex domains have complex requirements. Requirements are more than text. Text+data(state, ...) +graphics... +metadata. Engineers and customers live in a document-driven world that has to be reflected in tools. Need to distinguish what the customer wants(Laastenheft) from what the supplier is contracted to do(Pflichtenheft). Redundancy causes problems but is built in to the existing system. Good engineers are already content specialists in their special area and the content tends to evolve incrementally, so it pays to recycle old specifications. Takes time to migrate documents into a new requirements database. Details only appear at the leaves of the tree. Nonfunctional requirements, acceptance criteria and tests are not done well. Change is part of project life. Be ready to handle a lot of it. User-adaptable views help guide and manage a process. Specification reviews are important. Traceability is good: but what should be traced? Bad couplings between tools and text. We need better tools to manage requirements. Most of the problems are in areas that are not being researched. The real problem is managing the complexity not in expressing content and domain knowledge. .Close Weideetal94b .Open Weideetal94b Bruce W Weide & William F Ogden & Marli Sitaraman Recasting Algorithms to Encourage Reuse IEEE Software Magazine V11n5(Sep 1994)pp80-88 =ESSAY ALGORITHMS REUSE MACHINES .Box Algorithm becomes machine(state+smaller effect operations) ??virtual machine?? encapsulated objects and hidden objects. p82: "this basic idea has neither been touted as being as general as it is nor been further developped and systematically applied to the design of reusable software" p82: recasting a sort: "there are two distinct phases: and insertion phase and an extraction phase" (just like COBOL) "In our design neither the data's source nor its destination must be a certain data structure" p85: "Edges previuosly extracted could be made erroneous as new edges are inserted. This additional reason supports the logic behind making this a two-phse machine" (there is an order clash)(assembly line diagram of Orr). p87: "Machine-oriented design is easier for clients understand" p88:"First try to develop a simple, fully abstarct, clearly explainable mathematical model. Then consider if you can settle for a two-phase mahine. You should probably have a two phase version of every machine in the reusable component library even if you can't see the immediate need for it in a particular case. Often, implementations for two-phase machines are easier to and/or potentially more efficient than for multiphase or haeless machines."... choose a design that is easily explained.... "what and when your machine does something will depend, in part, on which explanation is most understandable. You might have to use trial and error before you can judge which is best. But don't worry about the initial cost of making these design decisions! If you component is really reusable, the effort you spend on making a good design choice will be amortized over many future uses." .Close.Box .Close Weidenbach95 .Open Weidenbach95 Christoph Wiedenbach First-Order Tableaus with Sorts PostScript file Downloaded from internet, Max-Planck-Institue fur Informatik, Im Stadtwald, 66123 Saarbruken, Germany =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES demonstrates that tableaus - treestyle proofs - are shortened by adding types(sorts) as a special set of unary predicates and modfying two rules. The result is complete and sound. .Close Weidenback94 .Open Weidenback94 Christoph Weidenbach First-Order Tableaux with Sorts Submitted to IGPL usenet group June 1995 ftp://dcs.ox.ac.uk/sorttab.ps.g(??) =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES .Box Gensen style natural induction (cf hodges) extended by adding sorts to variables, Each variable has a set of sorts assoicated with it. Each sort is interprtted as a unary predicate. s(x)=finite@(U->@)... for all x (p) +> for all x ( if and(s(x)(x)) then p). for some x (p) +> for some x ( and(s(x)(x)) and p). Modified derivation rules for all x (p(x)), and( s(x)(t) ), t any term |- P(t) for some x (p(x)), new v |- p(v), and( s(x)(v) ) Gives much simpler proofs Proved to be as complete and consistent as the original .Close.Box .Close Wells95 .Open Wells95 Charles Wells Communicating Mathematics: Useful Ideas from Computer science Am Math Monthly V102n5(May 1995)pp397-408 =ESSAY MATHEMATICS .Box function Doamain->Bool as external behavior Sets are a way to represent other things. specify external behavior rather than set theoretic representations when introducing ideas. Distinguish syntax from semantics: expression vs what it denotes, ainformal parsing, make types explicit Formal transformations: definitions as macros, proof by rewriting(GriesSchneider95), give syntactic and semantic proof., mental representations, make logic explicit. Types and polymorphism. distinguish function, its vlaues, an algorithm that implemnts it. Self-montoring:give mistakes a name. give punchy names for good behaviours, go for high context communitcation .Close.Box .Close Whangetal92 .Open Whangetal92 Kyu-Young Whang & Ashok Malhotra & Gary H Sockut & Luanne Burns & Key-Sun Choi Two-Dimensional Specification of Universal Quantification in a Graphical Database Query Language IEEE Trans SE-18n3(Mar 1992)pp216-224 =ADVERT GRAPHIC DATA LOGIC .Close WhiteheadRussell63 .Open WhiteheadRussell63 Alfred North Whitehead & Bertrand Russell Principia Mathematica(2nd Edition) Vol 1 OUP UK: Oxford University Press England 1963 =CLASSIC logic RELATIONS SETS PREDICATES structures regular TYPES dotty notation and fun typographical symbols. Attempting to show that the whole of mathematics is a subset of formal logic. To resolve paradoxes introduced the theory of types. To make type system work invented generic expressions "Typical ambiguity". Interesting model of induction and the theory of "..." via transitive closures. Republished as .See [WhiteheadRussell97] .Close WhiteheadRussell97 .Open WhiteheadRussell97 Alfred North Whitehead & Bertrand Russell Principia Mathematica to *56 Cambridge University Press UK1997 =FORMAL LOGIC TYPES PREDICATES CLASSES RELATIONS PROOFS MATHEMATICS Facsimile of the beginning of the original 1927 `magnum opus` going from the propositional calculus to the definition of the numbers 0, 1, & 2! PM::="Principia Mathemtica by Russell and Whitehead, 1927, ... ". Attempts to construct traditional mathematics in formal symbolic logic. Earlier edition .See [WhiteheadRussell63] from Oxford University Press. .Close WidomGriesSchneider92 .Open WidomGriesSchneider92 Jennifer Widom & David Gries & Fred B Schneider Trace-based Network Proof Systems: Expressiveness and Completeness ACM Trans Program Lang Syst(TOPLAS)V14n3(Jul 1992)pp396-416 CR9302-0090 =THEORY CONCURRENT SNL=Simple Network Logic Predicates over traces, sound but incomplete, needs the addition of temporal ordering and prefix properties. .Close WilsonF00 .Open WilsonF00 Fred Wilson The Logic and methodology of science and pseudo-science Canadian's Scholars Press Inc, Toronto Ont CA 2000 ISBN 1-55130-175-X Q175.W66 2000 =FORMAL LOGIC SCIENCE HISTORY THEORY DATA .Close WingNixon89 .Open WingNixon89 Jeanette M Wing & M R Nixon Extending Ina Jo with Temporal Logic IEEE trans on Soft Eng SE-V15n2(Feb 1989)pp181-197 =ADVERT formal specification .Close WingVaziri-Farahani95 .Open WingVaziri-Farahani95 Jeanette M Wing<wing@cs.cmu.edu> & Mandana Vaziri-Farahani Model checking software systems: A Case study in .See [Kaiser95] =CASE-STUDY SQA FORMAL CASE-STUDY LOGIC It is feasible to check for some properties of non-finite state systems. When does ( p(a) imply (for all x(p(x))))? .Close Woodcock89b .Open Woodcock89b JCP Woodcock Calculating Properties of Z Specifications ACM SIGSOFT Software Engineering Notes v14n5(Jul 1989)pp43-54 =DEMO MATHEMATICS Z formal logic structures .Close Wordsworth96 .Open Wordsworth96 J B Wordsworth Software Engineering with B Addison-Wesley Longman Reading MA 1996 ISBN0-201-40356-0 CR9709-0632(D.2.1) =TEXTBOOK undergraduate TOOLs B MATHEMATICAL LOGIC .Close Wos98 .Open Wos98 Larry Wos Programs that offer Fast Flawless Logical Reasoning Commun ACM V41n6(Jun 1998)pp87-95 =ADVERT LOGIC TOOL not AI but rules and algebra OTTER::=http://www.mcs.anl.gov/home/mccune/ar/ database+inference+paramodulation+hyperresolution etc p93: "axiomatization" and representation in the program's language can be trying& even formidable .Close XiaLee0 .Open XiaLee0 Weidong Xia & Gwanhoo Lee Grasping the Complexity of IS Development projects Commun ACM V47n5(May 2004)pp69-74 =POLL COST TIME USER FUNCTION NONTECHNICAL distinguishes organizational from technological Complexity. Finds organizational complexity has the most effect. .Close Yamazakietal93 .Open Yamazakietal93 Seichi Yamazaki & Kiyohiko Kajihara & Mitsutaka Ito & Ryuichi Yasuhara Objected-oriented Design of Telecommunication Software Special Theme "Making OO Work" IEEE Software V10n1(Jan 1993)pp81-87 =EXPERIEMENT OBJECT-ORIENETD ROOD Real-time vs FD Object models==<{logical model, integration model} vs Physical model, Static(ER)+dynamic(FSM)+message sequences, Case study compared OO(in Ada 83)+FD on 10K LOC: OO gave greater extendabillity, lesser performance, more smaller and simpler modules (No inheritance), difficult to grasp the entire model and check consistency. .Close YangHawblitzel11 .Open YangHawblitzel11 Jean Yang & Chris Hawblitzel Safe to the last instruction: Automated verification of a type-safe operating system Commun ACM V54n12(Dec 2011)pp123-131 .See http://doi.acm.org/10.1145/2043174.2043197 =ADVERT LOGIC PROOF TOOLS SAFETY MEMORY OSs Kernel Nucleus Typed Assembly Language TAL Verve Hoare C# Demonstrates feasibility of developing a proved type-safe operating system. .Close Young97 .Open Young97 William D Young Comparing Varification Systems: Interactive Consistency in ACL2 IEEE Trans Softw Eng VSE23n4(Apr 1997)pp214-223 =DEMO PROOF LOGIC LISP .See [ACL2] .See [KaufmanMoore97] hardware CLI advantages of no types and LISP-like notation vs .See [PVS] Rushby .Close Young07 .Open Young07 Chelsea Anne Young Spreadsheets using logic instead of math may revolutionize data management =ADVERT LOGIC TOOL Standford Logic Group .See http://news-service.stanford.edu/news/2007/april25/logic-042507.html Quote "There are many cases where traditional spreadsheets are just not sufficient," says Associate Professor Michael .Key Genesereth , whose group in the Computer Science Department is developing this new method of data management. "Why not have a spreadsheet that looks just like a regular spreadsheet except it has the ability to encode and use logical formulas? That's what you can't do with Excel in any way today." .Close Yourdon07 .Open Yourdon07 Ed Yourdon Celebrating Peopleware's 20th Anniversary IEEE Software Magazine V24n5(Sep/Oct 2007)pp96-100 =HISTORY PEOPLE =REPORT PANEL Boehm Brooks Rising Lister DeMarco The major problems with software development are sociological not technical. .Close Zadeh94 .Open Zadeh94 Lotfi A Zadeh Fuzzy Logic, Neural Networks, and Soft Computing Comm ACM V37n3(Mar 1994)(AI issue)pp77-86 =ADVERT FUzzY LOGIC .Close ZaveJackson93 .Open ZaveJackson93 Pamela Zave<pamela@research.att.com> & Michael A Jackson Conjunction as Composition ACM Trans on Softw Eng & Meth V2n4(Oct 1993)pp379..411 CR9408-0546 =DEMO FORMAL REQUIREMENTS SPECIFICATION .Box Note Multi-paradigm specifications, more in Jackson95x Must have common semantics. So assume first order logic. Model types as one-place predicates. Kleene's notation..., Z , prolog,.... Renaming to couple and instanciate specifications. Distinguish defined from undefined terms. ?? Problem with recursive predicate definitions Must form a DAG statements equivalent to .As_is for all p:Projects, one m:EMPLOYEE(m leads p). member(x,y) := x \in y sequences modeled as totally order sets of events. Net{member::@event, preceeds::@(event,event)... initial, final,...} .Close.Box .Close ZaveJackson96 .Open ZaveJackson96 Pamela Zave<pamela@research.att.com> & Michael A Jackson Where Do Operations come From? A Multiparadigm Specification Technique IEEE Trans Soft Eng VSE-22n7(Jul 1996)pp508-528 =DEMO specification methods logic std Z better than .See [ZaveJackson9X] .See [ZaveJackson93] .Close ZaveJackson9X .Open ZaveJackson9X Pamela Zave & Michael A Jackson Where Do Operations come From? Specification of Event Properties Preprint received Pamela Zave 1993 - Submitted for publication 1993. Published as .See [ZaveJackson96] =DEMO Multiparadigm specification GRAPHIC Z STDs Jackson diagrams predicate LOGIC sequences input events occurring at multiple events need to be mapped into central operations in a central specification incomprehensible graphical notation for case analysis(fig 4) is not in .See [ZaveJackson96] .Close ZellerSnelting97 .Open ZellerSnelting97 Andreas Zeller & Gregor Snelting Unified Versioning through Feature logic ACM ToSEM V6n4(Oct 1997)pp398-441 =THEORY =TOOLS SCM feature logic defined in Smolka92 J Logic Programming .Close Zelkowitz94 .Open Zelkowitz94 Marvin V Zelkowitz<mvz@cs.umd.edu> Algebra and Models ( and Reality) ACM SIGSOFT Software Engineering Notes v19 n10(Oct 1994 1995)pp79-81 & V20 n4 (Apr 1995)pp55-57 =CRITIQUE HOARE LOGIC PROGRAM States the algebra of Hoares algebra of programs quotes .See [Hoare69] and Hoare in 1993 argues that since on some machines x'=x+1 does not implie x'>x on all machines that modern mathematics shouldn't be used. Appeals for a (as yet) unknown approach based on natural science. "There needs to be feedback" .Close Zhang91 .Open Zhang91 Guo-Qiang Zhang Logic of Domains Birkhauser Boston Inc Cambridge MA 1991 ISBN 0-8176-3570-X CR9303-0126(D.2.2) =THEORY Semantics SFSS SFP. cpos<==SFP<==scott<==stable domains. .Close ZowghiOffen97 .Open ZowghiOffen97 Didar Zowghi & Ray Offen A Logical Framework for Modeling and Reasoning about the Evolution of Requirements RE'97 pp247-257 .See [RE'97] =THEORY REQUIREMENTS EVOLUTION AGM nonmonotonic logics |~ epistemic entrenchement AGM .Box .See [Gadenfors88] P Gardenfors, Knowledge in Flux: Modeling the Dynamics of Epistemic States'. MIT Cambridge MA 1988 .Close.Box .Close

Search for bibliographic items containing a matching string.

To see the complete bibliography (1Mb+) select:[Bibliography]