[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> bib
|| [News] || [Research]

Bibliography Retrieval Engine(Beta)

Items in bibliography identified by a string matching Z

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

Abowdetal93
.Open Abowdetal93
 Gregory D Abowd & Robert Allen & David Garlan
 Using Style to Understand Descriptions of Software Architecture
 In 
.See [Notkin93]
pp9-20
 =THEORY MATHEMATICAL ARCHITECTURE
 Z Pipe-filter and Event System styles
 partial functions Syntax<>->Semantics to describe constraints on syntax
.Box
pipe-filter
Abstract syntax{ports, descriptions, roles, connections, components, connectors, attachments}

-ve: some small Z errors
-ve: Includes filter's state as part of model of filter. amow: should use IO relations

Event-System style: invoked, announced, methods, events, states, start,... NOT classes

Analysis, special cases,....
.Close.Box
.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

AdcockEtAl07
.Open AdcockEtAl07
 Bruce Adcock & Paolo Bucci & Wayne D Heym & Joseph E Hollingsworth & Timothy Long 
 Which Pointer Errors do Students Make?
 ACM SIGCSE Bulletin V39n1(Mar 2007) & proc SIGCSE'07 pp9-13
 =ADVERT TOOL C++ Java PEDAGOGY
 Proposes finite state models for pointers in C++ and in Java.
 Java_pointer_model::=following
.Table Old\New	Alive	Null	Out of scope
.Row Alive	* new	NULL	}
.Row Null	new	NULL *X	}
.Row Out of scope	0	0	declare
.Close.Table
(X = unsafe)
 C++Pointer_model::=following
.Table Old\New	Alive	Null	Out of scope	Dead
.Row Alive	* new Z	NULL Z	} Z	delete \epsilon
.Row Null	new	NULL *X delete	}	0
.Row Out of scope	0	0	0	declare
.Row Dead	new	NULL	}	* X delete X
.Close.Table
(Z=dangerous, X=unsafe, \epsilon=spontaneous)
.Close

AlexanderH88
.Open AlexanderH88
 Heather Alexander
 Comments on "Formal Specification of User Interfaces: A comparison and Evaluation of Four Axiomatic Approaches"
 IEEE Trans Soft Eng VSE-14n4(Apr 1988)pp438-439
 =DEMO need SQA on Z SPECIFICATIONs as well as code
.Close

AltendorfHohmanZabicki02
.Open AltendorfHohmanZabicki02
 Eric Altendorf & Moses Hohman & Roman Zabicki
 Using J2EE on a large, Web-Based Project
 IEEE Software Magazine V19n2(Mar/Apr 2002)pp81-89
 =EXPERIENCE WEB/NET MODULE COMPONENT JAVA J2EE
.Close

Ambleretal92
.Open Ambleretal92
 Alan L Ambler & Margaret M Burnett & Betsy A Zimmerman
 Operational Versus Definitional: A Perspective on Programming Paradigms
 IEEE Computer v25n9(Sep 1992)pp28-43
 =DEFINITION TECHNICAL LANGUAGES
.Close

AndrewsZhang03
.Open AndrewsZhang03
 James Andrews & Yinqjun Zhang
 General Test Result Checking with Log File Analysis
 IEEE Trans Software Engineering  V29n7(Jul 2003)pp634-648
 =EXPERIMENT RANDOM TESTING LOG TIMED FSM  LFA lift language LFAL Prolog dictionary ADT
 SUT::="Software Under Test".
 LFA::="Log file analysis"..
.Close

Ardisetal96
.Open Ardisetal96
 Mark A Ardis & John A Chaves & Lalita Jategaonker Jagadeesan & Peter Mataga & Carlos Puchol & Mark G StasKauskas & James Von Olnhausen
 A Framework for Evaluating Specification Methods for Reactive Systems: Experience Report
 IEEE Trans Softw Eng VSE22N6(Jun 1996)pp378-389 revised from ICSE-17 1995
 =COMPARISON Modechart VFSM Esterel LOTOS Z SDL C telecommunications; SDL and Esterel scored well
 methods uncovered dangerous ambiguity in an informally stated standard
.Close

ArcuriZohaibBrand12
.Open ArcuriZohaibBrand12
 Andrea Arcuri & Muhammad Zohaib & Lionel Brand
 Random Testing: Theoretical results and practical implications
 IEEE Trans Software Engineering  V38n2(Mar/Apr 2012)pp258-277
& ISSTA 2010
 =SURVEY PROBABILITY  TESTING ORACLES SUT COUPON COLLECTOR RT 
 Good introduction to the topic.  Covers the background and history well. 
 Proves several neat theorems. 
 Traditionally random testing is thought to be worse than partition testing.
 This paper surveys experience papers and the theory to argue that it is not as bad as we thought. 
.Close

Armour10
.Open Armour10
 Phillip G Armour
 Return at Risk
 Commun ACM V53n9(Sep 2010)pp23-25
.See http://doi.acm.org/10.1145/1810891.1810902
 =POLEMIC ESTIMATION ROI RISK COST VALUE DISTRIBUTION 
ROI::acronym="Return on Investment"
 Argues that the traditional straight line formula
      ROI=(value-cost)/cost,
is not valid if there is any risk of the cost or value being wrong. 
 Need cost and value profiles. Probability distributions. 
 Notes that `cost' tends to be skewed toward overruns and `value` towards zero.  
 Calculating a better likely or average ROI is not simple and may need Monte Carlo methods. There exist tools.
 Are cost and value independent?
.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

Bankeretal93
.Open Bankeretal93
 Rajiv D Banker & Srikani M Datar & Chris F Kemerer & Dani Zweig
 Software Complexity and Maintenance Costs
 Comm ACM V36n11(Nov 1993)pp81-94
 Maintenance Time increased by larger modules & larger paragraphs & "bad" GOTOs
.Close

BarnettEtAl11
.Open BarnettEtAl11
 Mike Barnett & Manuel Fahndrich & K Rustin M Leino & Peter Muller & Wolfram Schulte & Herman Venter
 Specification and Verification: the Spec# Experience
 Commun ACM V54n6(Jun 2011)pp81-91
.See http://doi.acm.org/10.1145/1953122.1953145
 =ADVERT CONTRACTS MICROSOFT C# .NET IDE SPECIFICATION LANGUAGE Spec# TOOLS PRECONDITIONS POSTCONDITIONS INVARIANTS Boogie CCI Z3 PROOFS
.Key Spec#
 Planned to hide the proofs from the programmers!
 Contracts written in the programming language.
 Display contract as a tool-tip on a call.
 Treat static mismatched conditions as if they were syntax errors.
 Distinguishes between pointers and guaranteed non-null pointers.
 Provide static and dynamic checking of conditions.
 Can supply many loop invariants automatically.
 To be useful it must be integrated into a real language and IDE.
.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

Barrett95
.Open Barrett95
 Geof Barrett
 Model Checking in Practice: The T9000 Virtual Channel Processor
 IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp69-78
 =EXPERIENCE SQA INSPECTIONS MODEL CHECKING FORMAL NOTATIONS STD CSP Z English
 Sometime implementation was correct when the spec was wrong
 Easier to show what can happen than to show that something can not happen
 Problem with notation(CSP) - "completely alien" to people used to STDs.
 Quote: "Must base our tools on familiar notations and understand the obstacles...this means that visual specifications have to be used as much as possible."
 Using multiple notations. STDs+Z+English.
 Using checker for finite sequences.
 Need an unusual combination of engineering, mathematical and programming skills
.Close

BasiliMcGarryPajerskiZelkowitz02
.Open BasiliMcGarryPajerskiZelkowitz02
 Victor Basili & Frank E McGarry & Rose Pajerski & Marvin V Zelkowitz
 Lessons learned from 25 years of process improvement:  the rise and fall  of the NASA software engineering laboratory
 ICSE24(May 2002)pp69-79  $CR 0406-0749
 =UNREAD =HISTORY IMPROVEMENT NASA SEL
 Need management & staff support + focus & data.
.Close

GrafLormansToetenel03
.Open GrafLormansToetenel03
 Bas Graf & Marco Lormans & Hans Toetenel
 Embedded Software Engineering: The State of the Practice
 IEEE Software Magazine V20n6(Nov/Dec 2003)pp61-69
 =POLL 36  INTERVIEWS EMBEDDED REQUIREMENTS ARCHITECTURE MOOSE ITEA UML
 Hardware driven, top-down: system drives subsystem drives component. At each stage the previous architecture becomes a requirement in the next level.
 Stakeholders ={manufacturing, maintenance, marketing(users/consumers)}.
 Context = { Suppliers, standards, legacies, regulators }
 Requirements expressed in text using word processors and templates. Informal diagrams.  Use cases from the UML. Some sequence diagrams and domain models.  Pre/post conditions in programming.  Only one formal specification(in Z).
 Managing changing requirements: spreadsheets.
 Architecture: vs time-to-market. Creative.
 Performance: design for maximum speed possible, hope, and test.  UML popular with Visio and Rose.  DFDs. ERDs. HatleyPirbhai.
 Reuse: Ad hoc.
 Memory, power and real time less prominent than expected.
 Modern methods/technologies: vs legacy systems, are too immature and complex,
.Close

BassNordWoodZubrow06
.Open BassNordWoodZubrow06
 Len Bass & Robert Nord & William Wood & David Zubrow
 Risk Themes Discovered Through Architecture
 =EXPERIENCE RISK ARCHITECTURE ATAM QUALITY
 Tech Report CMU/SEU-2006-TR-012
 ATAM::="Architecture Tradeoff Analysis Method".
 Lists 15 Risk Theme Categories: Availability, Performance, security, modifiability, integration, process and tools, requirements, allocation, documentation, Big Picture, Unrecognized needs, product lines, awareness, scope, coordination.
 Claims 99 risk themes.
 Reference to Boeing experience with ATAM and Charette's failure causes.
 Relation to business goals.
 Importance of "Performance" .
 No evidence that risks are independent of domain. One size does not fit all.
 Risks of commission and Omission.  Omission more common.
 Odd fact: security was always a risk of omitting to do something.
.Close

BerglandZave86
.Open BerglandZave86
 Glen D Bergland & Pamela Zave
 Special Issue on Software Design Methods
 IEEE Trans on Software Engineering SE-12n 2 (Feb 1986)
 =survey object-oriented DAD JSD functional formal ADTs DFD
.Close

BernardLaffite99
.Open BernardLaffite99
 Pascal Bernard & Guy Laffite
 The French Population Census for 1990
 In 
.See [HincheyBowen99]
pp15-42
 =EXPERIENCE MATH Z B METHOD REQUIREMENTS GEOGRAPHY CENSUS
 It worked as a process and a product.
.Close

BiemanZhao95
.Open BiemanZhao95
 James M Bieman(bieman@cs.colostate.edu) & Josephine Xia Zhao
 Reuse Through Inheritance: A Quantitive study of C++ Software
.See [SamadzadehZand95] pp47-52
 Inheritance is used far less frequently than expected
.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

BloomChengDsouza97
.Open BloomChengDsouza97
 Bard Bloom & Allan Cheng & Ashvin Dsouza
 Using a Protean Language to Enhance expresiveness in Specifications
 IEEE Trans Softw Eng VSE23n4(Apr 1997)pp224-234
 Using structural Operational semantics to construct and extend specification languages including CCS Z Petri nets. GSOS Simple BDD-based model checking. philosphers & lifts
.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

Blum94
.Open Blum94
 Bruce I Blum
 A Taxonomy of Software Development Methods
 Commun ACM V37n11(Nov 1994)pp82-94 CR9602-0143
 history(pp84-90) methods
.Box
Design methods include analysis...code.
All based on ideas started in 1968-1977.
No clear dividing lines between successive activities
shift from life cycle to process
Destinguishes: descriptive models("conceptual")(give guidance) from prescriptive models("formal")(establish criteria).
and: problem oriented(focus on understanding the problem/solution) from product oriented(correct transformation from a prescription to a maintainable implementation).
Four categories.
problem oriented prescriptive models have potential
automatic support for product oriented formal
problem oriented tend to be descriptive and prescriptive tend to be product oriented.

Mentions levels of abstraction, virtual machines, SWR, functional decomposition, structured design, coupling, cohesion, structure chart, information hiding, structured programming, proofs of correctness, algebraic specification, ADTs, structured analyisi, DFDs PSL/PSA, ERM(ERD), STD. petrie nets, warnier LCS (not LCP), JSP, JSD, VDM (not Z), OOP, OOA, Modern structured analysis, no silver bullets.
?? mathematical means top-down?
isomorphism between problem and solution
tension in development between need for subjective designs and formal programs.... top-down vs outside in, data flow vs data structure.
.Close.Box
.Close

Bolognesi00
.Open Bolognesi00
 Tommaso Bolognesi
 Toward Constraint-Object-Oriented Development
 IEEE Trans Software Engineering  V26n7(Jul 2000)pp594-616
 =EXAMPLE OBJECT-ORIENTED SPECIFICATION DESIGN STYLE  COO LOTOS CO-NOTATION Z GRAPHIC
.Close

BoltaciJones95
.Open BoltaciJones95
 L. Boltaci & J.Jones
 Formal specification using Z: A modeling approach
 International Thomson Publishing London 1995.
 =DEMO MODEL Z SPECIFICATION FORMAL
.Close

BorgidaMylopoulosReiter93
.Open BorgidaMylopoulosReiter93
 A Borgida & J Mylopoulos & R Reiter
 "And Nothing Else Changes":The frame problem in procedure specifications
 In Proc of the 15th Int Conf on Software Engineering
 IEEE Computer Society(May 1993)pp303-314
 Ref from ZaveJackson93
.See [Borgidaetal95]
.See [BicarreguiRitchie95]
.Close

Boswell95
.Open Boswell95
 Anthony Boswell
 Specification and Validation of a Security Policy Model
 IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp63-68
 =ADVERT TOOL FORMALIZER and Z
.Box
typical Z schemas are 6..10 lines long,
65 schemas in total
some here where 11..20 or more
giant schemas: many definitions, state transitions, state includes state of many tables.

systematic documentation of results and structure of arguments

The usefulness of diagrams...systematic diagrams.
.Close.Box
.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

BowenHinchey95b
.Open BowenHinchey95b
 Jonathan P Bowen & Michael G Hinchey
 Seven More Myths of Formal Methods
 IEEE Software Magazine V12n4(Jul 1995)pp34-40
.Box
Note Based on industrial experience
Ref to 
.See [Hall90]
 8. FM delay the development process
 9. FM lack tools
 10. FM replace traditional engineering design methods
 11. FM only apply to software
 12. FM are unnecessary
 13. FM are not supportted
 14. FM people always use FM
 p40: "system development should be as formal as necessary, but not more formal."

Notes problems:
  sidebar, p37: defining FM, IEEE glossary has two.
  notation

p38: Notes resources: internet forums for Z, VDM, Larch, OBJ.  FTP archives, Periodicals. Courses.

p40: Quotes BBC Interview: "If you want to build systems with ultra-high reliability whcih provide complaxe functionallity and you want to guarantee that they are going to work with very high reliability...you can't do it"
.Close.Box
.Close

BowenHinchey06
.Open BowenHinchey06
 Jonathan P Bowen & Michael G Hinchey
 Ten Commandments of Formal Methods ... Ten years later
 IEEE Computer Magazine  V39n1(Jan 2006)pp40-48 
 =HISTORY FORMAL Z TLA 
 See also "The Ten Commandments revisited: a ten-year perspective on Industrial application of formal methods" Proc 10th Int'l Workshop on formal methods for industrial Critical Systems, ACM Press 2005 pp8-16
 CF
.See [BowenHinchey95a]
.Table Then     Now
.Row I. Thou shalt Choose an Appropriate Notation.
.Item More now. Hybrids.
.Row II. Thou shalt Formalize but not Overformalize.
.Item 3 levels: specs, Proofs, machine checked.
.Row III.  Thou shalt Estimate Costs.
.Row IV. They shalt have a Formal Methods Guru On Call.
.Item Plus a domain expert early on.
.Row V. Thou shalt not Abandon Traditional methods.
.Row VI. Thou shalt Document Sufficiently.
.Item Iterative.  Including why & when decided.
.Row VII. Thou shalt not Compromise thy QUALITY Standards.
.Item Notation & method.
.Row VIII. Thou shalt not be Dogmatic.
.Item Gap between analysis & specification.
.Row IX Thou shalt Test, Test, and Test again.
.Row X. Thou Shalt Reuse.
.Close.Table
.Close

BowenReeves11
.Open BowenReeves11
 Jonathan P. Bowen & Steve Reeves
 From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community, 
 In Michael Butler and Wolfram Schulte (eds.), FM 2011: 17th International Symposium of Formal Methods. Springer-Verlag, LNCS, V6664(2011) pp308-322
.See http://issuu.com/jpbowen/docs/fm2011 
 =DEMO PROCESS COMMUNITY FORMAL METHODS Z BOK KNOWLEDGE
Abstract. 
.Box
A Body of Knowledge (BoK) is an ontology for a particular 
professional 
domain. A Community of Practice (CoP) is the collection of people 
developing 
such knowledge. In the paper we explore these concepts in the context 
of the formal methods community in general and the Z notation 
community, as 
has been supported by the Z User Group, in particular. The existing 
SWEBOK 
Software Engineering Body of Knowledge is considered with respect to 
formal 
methods and a high-level model for the possible structure of of a BoK 
is provided 
using the Z notation.
.Close.Box 
 The slides for the presentation are under: 
.See http://www.slideshare.net/jpbowen/fm-2011-symposium-slides 
 Translation of formal portion of slides (in Z) into MATHS:
.See ./samples/BoK.html
.Close

Brownbridge90
.Open Brownbridge90
 David Brownbridge(drb@paxis.co.uk)
 Using Z to Develop a CASE Toolset
 pp142-149 in Nicholls90
 =EXPERIENCE SSADM Z CASE 
 340 pages of Z -> 37KLOC object-oriented in 11 months
 no need of refinement
 needed for typechecker
 formal specification reviews are needed
 needed roadmap of hierarchy
.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

Bryant90
.Open Bryant90
 Tony Bryant
 Structured methodologies and formal notations: Developing a framework for synthesis and investigation
 pp229-241 in Nicholls90
 =THEORY Z SSADM DEF STAN 0055
.Box
Chapter 2 section 4.1 clash between rigid method and dynamic system page 231
.Close.Box
.Close

BrylowPalsberg04
.Open BrylowPalsberg04
 Dennis Brylow & Jens Palsberg
 Deadline Analysis of Interrupt-Driven Software
 IEEE Trans Software Engineering  V30n10(Sep 2004)pp634-655
 =DEMO Formal TIMING Z86 Interrupt Handling TEST
.Close

Cardenas-GarciaZelkowitz91
.Open Cardenas-GarciaZelkowitz91
 Sergio Cardenas-Garcia & Marvin V Zelkowitz
 A Management Tool for Evaluation of Software Designs
 IEEE Trans SE-16 n9(Sep 1991)p961-971. QUALITY+PURPOSE risk analysis
 viabillity::=correct+weighted attributes
.Close

CardZubrow01
.Open CardZubrow01
 David Card & David Zubrow
 benchmarking software organizations
 IEEE Software Magazine V18n4(July/Aug 2001)pp16-17
 =EDITORIAL BENCHMARKING PROCESSES CMM
 Difficult: define clear objectives, plan carefully, and interpret cautiously.
  For more see pages18-56
.Close

CarringtonDukeHayesWelsh93
.Open CarringtonDukeHayesWelsh93
 David Carrington<davec@cs.uq.oz.au> & David  Duke<duke@minster.york.ac.uk> & Ian Hayes<ianh@cs.uq.oz.au> & Jim Welsh<jom@cs.uq.oz.au>
 Deriving Modular Designs from From Specifications
.See [Notkin93] pp 89-98
 =CASE-STUDY FORMAL Design Z
.Box
Case study: UQ2 generic editor of structured documents.

finding dependencies, gnerating clusters, NuProlog, tools set for analysis of Z etc

Formula for cohesion and closeness(roughly cohesion)

promotion can hide the simplicity of connections at lower levels.  Example p92-93...
tables with rd, wr, ...
.Close.Box
.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

Chaochenetal91
.Open Chaochenetal91
 Zhou Chaochen & C. A. R. Hoare & A. P. Ravn
 A calculus of durations
 Information Processing Letters V40( 1991)pp269-276
 =MATHEMATICAL model of Time
.Close

ChelfEbert09
.Open ChelfEbert09
 Ben Chelf & Christof Ebert 
 Ensuring the integrity of embedded software with static code analysis
 IEEE Software Magazine V26n3(May/Jun 2009)p96-99
 =ADVERT RISKS =HISTORY TOOLS lint
 p97 Links to resources in sidebar.
 Six_detectable_defect_classes:= division by zero + memory leak + null pointer dereference + uninitialized variable + buffer overflow or underflow +inappropriate cast.
.Close

ChenTseZhou02
.Open ChenTseZhou02
 Tsing Yueh Chen & T H Tse & Zhi Quan Zhou 
 Semi-Proving: an Integrated Method Based on Global Symbolic Evaluation and Metamorphic Testing
 Proc ISSTA02 & ACM SIGSOFT Software Engineering Notes V27n4(Jul 2002)pp190-195
& IEEE Trans Software Engineering  V37n1(Jan/Fed 2011)pp109-125 
 =EXAMPLE SYMBOLIC TESTING INVARIANT PROPERTIES TOOL METAMORPHIC RELATION PATHS
 Symbolically execute all paths to verify invariant results under changes of input.
  Example1: all permutations of 3 numbers have the same median.
 A mutated program will not satisfy the same test.
 Note: the IEEE Trans paper is extended and has title
"Semi-proving: an integrated method for program proving, testing, and debugging".
.Close

ChoiZeller02
.Open ChoiZeller02
 Jong-Deock Choi & Andreas Zeller 
 Isolating Failure-Inducing Thread Schedules
 Proc ISSTA02 & ACM SIGSOFT Software Engineering Notes V27n4(Jul 2002)pp210-220
 =DEMO TOOL TECHNIQUE TESTING Delta-Debugging NONSEQUENTIAL DEJAVU JAVA  Jalapeno
 Tool found smallest difference in schedules that caused an error to occur.
 Based on
.Seeee ZellerHildebrandt02
.Close

ConcepcionZeigler87
.Open ConcepcionZeigler87
 Arturo I Concepcion & Bernard P Zeigler
 DEVS Formalism: A Framework for Hierarchical Model Development
 IEEE Trans Soft Eng VSE-14n2(Feb 1988)pp228-241
 =DEMO hardware performance top-down simulation formal graphics
.Close

Cone06
.Open Cone06
 Edward Cone
 Scott Rosenberg: What Makes Software So Hard
 CIO Insight (Jan 8th 2007) Zipf-Davis 
URL
.See http://www.cioinsight.com/article2/0,1540,2079462,00.asp
 =REVIEW EXPERIENCE Salon ITERATIVE
 Book: Dreaming In Code: Two Dozen Programmers, Three Years, 4,732 Bugs, and One Quest for Transcendent Software (Crown, 2007)
 "people have succeeded in creating amazing software systems that do work,
and do serve people's needs....So it's doable. But when you pick up the 
rock and look underneath the surface of every one of those systems, you 
find stories of delay and difficulty and problems. "
.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

CougerZawacki01
.Open CougerZawacki01
 D J Couger & R A Zawacki
 Motivating and Managing Computer Personel
 John Wiley 1980
 =POLL THEORY PEOPLE
.Close

Craigenetal93
.Open Craigenetal93
 Dan Craigen(dan@ora.on.ca) & Susan Gerhart(pl0183@mail.psi.net) & Ted Ralston(ralston@cli.com)
 An International Survey of Industrial Applications of Formal Methods
 2 Vols  National Technical Information Service Springfield Virginia 22161 1993 ( NIST GCR 93/626-V1 -V2 order  PB93-178556/AS+PB93-178564/AS Microfiche: A02 $12.50+ A03/$12.50)
 =SURVEY FORMAL METHODS EXPERIENCE
 Long survey of twelve case studies of the use of formal methods in
industrial projects. Volume 1 describes the purpose, approach, analysis, and
conclusions of the survey; Volume 2 describes the case studies.
 CSR Gypsy B Statecharts Z*5 Cleanroom RAISE FDM HP-SL(VDM+??)
.Close

CraigenMeiselsSaaltink99
.Open CraigenMeiselsSaaltink99
 Dan Craigen & Irwin Meisels & Mark Saaltink
 Analyzing Z specifications with Z/EVES
 In 
.See [HincheyBowen99]
pp255-283
 =DEMO SQA Z SPECIFICATION PROOF TOOL Z/EVES  SWP
  demo on Sliding Window Protocol and a simple password/user system.
 Short and simple introduction to Z.
.Close

CugolaNitoEtal96
.Open CugolaNitoEtal96
 Giampaolo Cugola & Elizabetta di Nitto & Alfonso Fuggetta & Carlo Ghezzi
 A Framework for Formalizing Inconsistencies and Deviations in Human-centred Systems
 ACM TOSEM V5n3(Jul 1996)pp191-230
 =THEORY USER REQUIREMNTS FORMAL Z: REALITY vs SYSTEM PETRIE GRAPHICS
.Close

DaCapo08
.Open DaCapo08
 Stephen M Blackburn & Kathryn S McKinley & Robin Garner & Chris Hoffman & Asjad M Khan & Rotem Bentzur & Amer Diwan & Daniel Feinberg & Daniel Frampton & Samuel Z Guyer & Martin Hirzel & Antony Hosking & Han Lee & J Eliot & B Moss & Aashish Phansalkar & Darko Stefanovic & Thoms VanDrunen & Daniel von Dineklage & Ben Wiedemann 
 Wake Up and Smell the Coffee: Evaluation methodology for the 21st century
 =ADVERT JAVA BENCHMARKs PERFORMANCE METRICS
 Commun ACM V51n8(Aug 2008)pp83-89
.See http://doi.acm.org/10.1145/1378704.1378723  
 Developing a useful benchmark is time consuming.
 Using them needs understanding of relevant workloads, good experimental design, and rigorous analysis.
 Benchmark research is underfunded.
.Close

DamonJacksonJha96
.Open DamonJacksonJha96
 Craig A Damon & Daniel Jackson & Somesh Jha
 Checking Relational Specifications With Binary Descision Diagrams
 Proc 4th ACM SIGSOFT 96 Symp on the Foundns of Software Eng: ACM SIGSEN V21n6(Nov 1996)pp70-80
 =DEMO MODEL CHECKING BDDs
 Z-like specs checked via testrolog-type diagrams
 BDDs::=Binary Decision Diagrams
.Close

DangleLarsenShawZelkowitz05
.Open DangleLarsenShawZelkowitz05
 Kathleen Coleman Dangle & Patricia Larsen & Michele Shaw & Marvin V Zelkowitz
 Software Process Improvement in Small Organizations: A Case Study
 IEEE Software Magazine V22n5(Nov/Dec 2005)pp68-75
 =CASE STUDY DSCS CMM
 (dick)|- when does software process improvement merge into business process reengineering?
 (dick)|- Rediscovers some trad systems analysis and design ideas.
 Discoveries:
.Set
 Processes and process improvement should address business goals not just CMM dogma,
 Choose the sequence of improvements to support needs not CMM KPAs.
 TANSTAAFL: Improvement needs resources.
 Test proposed improvements on selected projects and change them before expanding enterprise-wide.
 Ongoing activities should drive the plans for introducing new processes.
 Start formal reviews immediately to provide feedback to stakeholders.
 Divide improvements up and delegate.
 Assess experience with software processes and SP improvement.
.Close.Set
.Close

DeanHinchey95
.Open DeanHinchey95
 Neville Dean & Michael G Hinchey
 Introducing Formal Methods Through Role-playing
 Papers of the 26th SIGCSE Technical Symposium on Computer science Education: ACM SIGCSE Bulletin V27n1(Mar 1995)pp302-36
 =EDUCATION FORMAL Z
.Box
Note
.See http://www.anglia.ac.uk/~cdean/
deescribes Z
"there is no suitable text which prepares in the way that they need."..."it has been necessary to write a new book"[Dean96]
Tendency of studentss to use  clever formal techniques to give formal statements of ambiguous and incomplete requirements.

[students think] "the purpose of the exercise is to write a 'program' to include as many of the esoteric aspects of the notation that they can squeeze in"

student are angry working with simulation of real requirements(!)

force students to re-express clever (but wrong) Z specs in english until ambiguities show up.

Instructor must act the part of customer: dismissing formal specs, and forcing students to include English explanations.
.Close.Box
.Close

DeAntonellisZonta90
.Open DeAntonellisZonta90
 Valeria De De Antonellis & Bruta Zonta
 A Disciplined Approach to Office Analysis
 IEEE Trans SE-16n8(Aug 1990)pp822-828
 =DEMO System Reality
.Close

Deck01
.Open Deck01
 Michael Deck 
 Managing Process Diversity while Improving your Practice
 IEEE Software Magazine V18n3(May/June 2001)pp21-27 
 =EXPERIENCE IMPROVEMENT EVOLUTION CLEANROOM PEOPLE RISKS INCREMENTS ONE-SIZE CMM
 Even in one project "one size does not fit all" parts of the project.  For example inspection do not help you test a prototype algorithm for adequate performance.  Remotely executed software must be derived in the most rigorous zero-defect approach but locally executed software does not need this.
 People -- especially new ones -- are a prime risk factor.
 Diversity plan distinguishes three levels for each part of a process: Foundation, standard and advanced.
 A practice can be required, recommended, or optional.
.Close

DeLineVenoliaRowan10
.Open DeLineVenoliaRowan10
 Robert DeLine & Gina Venolia & Kael Rowan (Microsoft Research)
 Software Development with Code Maps
 ACM Queue(Jul 4 2010)
.See http://queue.acm.org/detail.cfm?id=1831329
& Commun ACM V53n8(Aug 2010)pp48-62
(Better pictures)
.See http://doi.acm.org/10.1145/1787234.1787250
 =ADVERT TOOL GRAPHIC TECHNICAL CODE VISUALIZATION HCI CODE MAP VISUAL STUDIO CODE CANVAS
 Another tool that generate graphic zoomable and editable images of code.
But a tool based on what programmers already did!
 A rare example of applying systems analysis to software engineering.
.Close

DeLineZelesnikShaw97
.Open DeLineZelesnikShaw97
 Robert DeLine & Gregory Zelesnik & Mary Shaw
 Lessons on Converting Batch Systems to Support Interactions
.See [ICSE'97]
 =Experience architecture evolution
 8 rules on page 203
 no ref to Jackson's work in 1975.
.Close

DeMarcoHruschkaEtAl08
.Open DeMarcoHruschkaEtAl08
 Tom Demarco & Peter Hruschka & Tim Lister & Suzanne Robertson & James Robertson & McManamin
 Adrenaline Junkies and Template Zombies: Understanding patterns of project behavior
 Dorset House, NY NY 2008 pp248 ISBN 0932633676
 =UNREAD PEOPLE PATTERNS PROJECTS PROCESSES
 Contributions needed --
.Hole DeMarcoHruschkaEtAl08
.Close

DesharnaisEtal98
.Open DesharnaisEtal98
 Jules Desharnais & Marc frappier & Ridha Khedri & Ali Mili
 Integration of Sequential Scenarios
 IEEE Trans SE V24n9(Sep 1998)pp695-678 CR9906-0431
 =THEORY RELATIONS Z SCENARIOS
 If pre(R)&pre(Q)=pre(R&Q) then demonic_meet(R,Q) ::= R&Q | Q~(pre(R)><post(Q)) | R~(pre(Q)><post(R)).
 Scenario as a digraph labelled by two kinds of relations: those describing environment actions and those defining system actions.
 Integration defined by union of environment actions and demonic meet of system actions.
 "the simple fact of formalizing a specification or a scenario is a step towards a better understanding of the system under consideration"
.Close

DevlinRosenberg96
.Open DevlinRosenberg96
 Keith Devlin & Duska Rosenberg(Brunel)
 Language at Work: analyzing communication breakdown in the workplace to inform systems design
 CSLI/Stanford Standford CA 1996 ISBN 1-57586-05101
 =EXPERIENCE SYSTEM MATHEMATICS: Situation theory
 LFZ::="Layered formalism and zooming".
.Close

DickKrauseCozens90
.Open DickKrauseCozens90
 A J J Dick & P J  Krause & J Cozens
 Computer Aided Transformations of Z into Prolog
 pp71-85 in Nicholls90
 =DEMO TOOL Z SPECIFICATION PROLOG PROTOTYPE
 prototype
 animation tool
 finds unintended non-determinism in Z specification
.Close

DongYangZhang07
.Open DongYangZhang07
 Jing Dong & Sheng Yang & Kang Zhang
 Visualizing Design Patterns in Their Applications and Compositions
 IEEE Trans Software Engineering V33n7(Jul 2007)pp433-453
 =DEMO TOOL VisDP UML PROFILE PATTERNS GRAPHICS WEB SERVICE XMI J2EE java.awt  
 Need to show how one object/class plays  many roles depending on the patterns.
 Defines an UML profile to show how classes/attributes/operations take part
in design patterns.
 Demonstartes the clutter that appears with different ways of displaying this information.
 Demonstrates a tool that will make design paterns visible as requested by
the user.
.Close

EaddyEtAl08
.Open EaddyEtAl08
 Marc Eaddy & Thomas Zimmermann & Kaitlin D Sherwood & Vibhav Garg & Gail C Murphy & Nachiappan Nagappan & Alfred V Aho 
 Do Crosscutting Concerns Cause Defects
 IEEE Trans Software Engineering  V34n4(Jul/Aug 2008)pp497-515  
 =EMPIRICAL ASPECTS REQUIREMENTS CONCERNS CROSS-cutting CODE QUALITY BUGS
 Requirements mapped into concerns.
 Reverse engineered concern->code map and the bug->code mapping and deduce concern->bug relationship in corpus of Java code.
 Defects tend to be associated more with wide-spread concerns than with total amount of code implementing a concerns.
.Close

EbringerThorneZheng00
.Open EbringerThorneZheng00
 Tim Ebringer & Peter Thorne & Yuliang Zheng
 Parasitic Authentication to Protecting Your E-Wallet
 IEEE Computer Magazine V33n10(Oct 2000)pp54-60
 =IDEA USER SECURITY
.Close

Endres93
.Open Endres93
 Albert Endres
 Lessons Learned in an Industristrial Software Lab
 IEEE Software Magazine V10n5(Sep 1993)pp58-61
.Box
How IBM Boeblingen reduced its error rate by a factor of 10 while doubling productivity and halving project duration.

Millions of lines of code.

Formal methods: VDM & Harlan Mills. Complete training.
Added tools.  Used method+tool to separate module specification from module implementation... hance C++ and Ada rather than a separate language for design

Reuse.  Has to be planned for.  Rules: encapsulation, parameterized, generalized.  Opposite of old technique.
Centrally maintained Boeblingen Building blocks - zero defects, in use through out IBM.

Process: Well documented, publicized (Radice) and now online.

Academe vs practice?  Also no sharing of practices.
.Close.Box
.Close

FeatherLamsweerde94
.Open FeatherLamsweerde94
 Martin S Feather & Axel van Lamsweerde(eds)
 Succeedings of the seventh  International Workshop on Specifiction and Design(IWSSD7)
 ACM SIGSOFT Software Engineering Notes V19n3(Jul 1994)pp18-20
.Box
Keynote: Tom Maibaum "Taking More of the Soft out of Software Engineering" - Engineers usually make successful use of standard predefined models that hide teh mathematics.
Requirements engineering, Colin Potts... Jackson<Jacksonma@attmail.att.com> and Zave.
Jackson: system is a virtual device, translate user's domain model  into evironmental events model.
Elicitation for a new libray problem
We deal with big, some would say, insoluable problems, such as the clarification of objectives...resolution of disagreements...validation.
How to elicit or define requirements in the first place.
Results: Set of notes, differeing perspectives, less than full agreement, "The experts did not descrine 'the' system that they wanted[...]but described many of the automation opportunities that were currently being provided"... many gaps and ambiguities.
Real time systems: separating environment from system.  "A front-end language, often graphical[...] is often used to produce an easy-to-understand specification of a real time system[...]automatically translated...more amenable to formal analysis
Concurrency: "Start by identifying the events that concern the interface between a system and its environment"..."'If it is not taught to sophomores, can we expect it to be used?'"
Formal Reasoning: "is becoming one of the key issues in many areas of software specification and design."
Design Methods and Software Architectures: design fragments, 5 kinds of architecture: Conceptual, Module Interconnection, Code, Executiton, Hardware. "Modeling the relationships among the components is useful for understanding a method"  [...] "The purpose of the process portion of design methods was to constrain human creativity."
.Close.Box
.Close

Feijs93
.Open Feijs93
 Loe Feijs(Philips Reearch Laboratories Eindvoven)
 A Formalization of Design Methods: A \lambda-calculus Approach to Systems Design with an Application to Text Editing
 Ellis Horwood Chichester West Sussex UK 1993
 ISBN 0-13-106113-5
 Reviews CR9408-0498  IEEE Software magazine V11n5(Sep 1994)p130 by Anthony Hall(Praxis)
.Box
Keywords:
COLD-K, VDM, Z, Designs as DAGS, black box and glass box properties.  Specification \square_less_than_equal Implementation

\lambda-\pi


.Close.Box
.Close

FentonKrauseNeil02
.Open FentonKrauseNeil02
 Norman Fenton & Paul Krause & Martin Neil
 Software Measurement: Uncertainty and Causal Modeling
 IEEE Software Magazine V19n4(Jul/Aug 2002)pp116-122
 =EXAMPLE STATISTICAL MODELS PROCESS PRODUCT Bayesian networks
 regression does not predict errors well in practice. A positive correlation overall can become negative when another factor is taken into consideration (Simpson's paradox 1899).
 (Bayes_theorem_simple): P(event given condition) = P(condition given event)*P(event)/p(condition).
  Causality modeled by graph(node=>events, arrows=>causes), cause mean that p(one given other) is non zero.
 Note: For a Bayesian Belief Network the formula is P(event given `set of causes`) not a set of P(event given `one cause`).
.See ./maths/math_22_graphs.html#BAYESIAN_NETWORK
 Shows how a distribution of defects depends on complexity and on the number of defects found and fixed in unit testing.
.Close

FloydCetal91
.Open FloydCetal91
 Christiane Floyd & Heinz Zu"llighoven & Reinhard Budde & Reinhard Kiel-Sawic (Eds)
 Software Development & Reality Construction
 Springer Verlag NY NY 1992
 ISBN 0-387-54349-X QA76.76D47S633
 Post-modern
.Close

FlynnHoverdBrazier90
.Open FlynnHoverdBrazier90
 Mike Flynn & Tim Hoverd & David Brazier
 Formaliser - an Interactive Support Tool for Z
 pp128-141 in Nicholls90
 PC/AT WYSIWYG windows to LATEX with parsing smalltalk and type checking
.Close

Foster77
.Open Foster77
 M A Foster
 The Game Players of Zan
 DAW books no. 236, Donald A. Wollheim New York NY 1977
 =FICTION cellular automata life
.Close

FowlerKobryn02
.Open FowlerKobryn02
 Martin Fowler & Cris Kobryn
 Customizing UML for Fun and Profit
 Software Development Magazine V10n7(Jul 2002)pp-
 =DEMO UML TABULAR stereotype metaclass tags constraints
 A Stereotype is defined as <<stereotype>>ing a <<metaclass>> in the UML meta-model.
 A Stereotype has a name, zero or more tags (attribute) and zero or more constraints.
 Use UML class diagram.  Use generalization for special kinds of previous stereotypes.
 Can Use table to list the stereotype, base class, parent, tags, constraints and description.
 Can use a table to specify tags by stereotype, type, multiplicity and description.
.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

FrickEtal00
.Open FrickEtal00
 A Frick & G Goos & R Neuman & W Zimmerman
 Construction of robust class hierarchies
 Software - Practice & Experience V30n5(May 2000)pp481-543
 =THEORY OBJECT-ORIENTED TECHNICAL MODULES INHERITANCE DESIGN
 no one design is robust, flexible and efficient.
 given priorities and specification then best hierarchy can be generated automatically.
.Close

FriesenJahnichenWeber97
.Open FriesenJahnichenWeber97
 Viktor Friesen & Stefan Jahnichen & Mathias Weber
 Specification of Software Controlling a Discrete-Continuous Environment
.See [ICSE'97]
 REALITY OOA Z with continuous variables. statecharts
.Close

Gannonetal93
.Open Gannonetal93
 John D Gannon & Jim Purtilo & Marvin V Zelkovitz
 Software Specification: A Comparison of Formal Methods
 Vol 5 in the Computer-Based Information Systems in Organizations Series Ablex Pub Corp 355 Chestnut Street Norwood NJ(201-767-8450 1993/in preparation
.Box
MS Text book?  ISBN Paper: 1-56750-034-X/ $24.50(Tentative)

Only VDM mentioned in Blurb
.Close.Box
.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

GaoChenToyoshimaLeung99
.Open GaoChenToyoshimaLeung99
 Jerry Z Gao & Cris Chen & YasuFumi Toyoshima & David K Leung
 Engineering on the Internet for Global Software Production
 IEEE Computer Magazine V32n5(May 1999)pp38-47
 =ADVERT TECHNICAL PROCESS WEB/NET
.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

Glass96
.Open Glass96
 Robert L Glass(Computer Trends)
 Formal methods are a surrogate for a more serious software concern
 IEEE Computer Magazine V29N4(Apr 1996}p19
.Box
changes subject to why academia and industry disagree about what software engineering is about.  Need an ongoing forum of academics and practitioners but banning zealots of all stripes.

Claims that Formal methods are underdefined, underevlauated, and may be in the wrong direction, and can not lead to any breakthough.
.Close.Box
.Close

GopalMukhopadhyayKrishnan05
.Open GopalMukhopadhyayKrishnan05
 Anandasivam Gopal & Tridas Mukhopadhyay & M S Krishnan
 The Impact of institutional forces on software metrics programs
 IEEE Trans Software Engineering  V31n8(Aug 2005)pp679-694
 =SURVEY STATISTICS METRICS PROCESS MANAGEMENT CUSTOMERS RIVALS
 Applies Cooper and Zmud's innovation diffusion model(1990) :
 innovation_diffusion ::= initiation; adoption; adaption; acceptance; routinization; infusion.
 Adaption is when the the normal processes are being changed to fit the innovation.
 Management, Customers, and rivals all influence whether a metrics program make it into/through adaption.
 See also
.See [GopalKrishnanEtAl02].
.Close

Gray88
.Open Gray88
 David Gray
 The Formal Specification of a Small Bookshop Information System
 IEEE Trans on Soft Eng vSE-14n2(Feb 1988)pp263-272
 =EXAMPLE PURPOSE Z
.Close

GreiskampLepper00
.Open GreiskampLepper00
 Wolfgang Grieskamp & Markus Lepper
 Using Use Cases in Executable Z
 3rd IEEE Int'l Conf Formal Engineering Methods (Sep 2000)pp111-119
 =DEMO FORMALIZE Black Box TEST USE CASES  Executable Z Notation Lift  ZAP ZETA
 Shows how to express use cases/scenarios in an executable form of the Z notation.
.Close

GunterGunterJacksonZave00
.Open GunterGunterJacksonZave00
 Carl A Gunter & Elsa L Gunter & Michael A Jackson & Pamela Zave
 A Reference Model for Requirements and Specifications
 IEEE Software Magazine V17n3(May/Jun 2000)pp37-43
 =THEORY REQUIREMENTS SPECIFICATION REALITY WRSPM
 W, R, S refer to the environment. S, P, M refer to the system.
 Actual expression of descriptions can take many forms.
 Designated terms -- typically designate states, events, and/or individuals.
`e` -- controled by environment, `s` -- controled by system.
 Shared terminology.
 Three properties of adequacy and consistency define a contract between the
buyer and seller of the software.
 Similar, relative, properties constrain the specification and imply the
three fundamental properties.

.See http://www/dick/notes/GunterGunterJacksonZave00.html
 See also 
.See [ZaveJackson97b]
.Close

HalaszSchwartz90
.Open HalaszSchwartz90
 Frank Halasz & Mayer Schwartz
 The Dexter Hypertext Reference Model
 Proceedings of the Hypertext Workshop NIST Gaithersburg Md Jan 16-18 1990
 NIST Special Publication 500-178 March 1990 pp95-133
 =EXPERIENCE FORMAL Dexter WWW/NET Z
.Close

Hales08
.Open Hales08
 Thomas Hales
 Formal Proof
 Notices of the American Mathematical Society V55n11 (Dec 2008)
.See http://www.ams.org/notices/200811/tx081101370p.pdf
 =EXAMPLES HOL Light FORMAL PROOFS MATHEMATICS ZFC TYPES
 Good discussion of the philosophy of formal proofs and HOL Light in particular.
 Difficult theorems can have 1728 pages for an informal proof and take decades to write.
 Provide formalizations can take years.
 DeBruijn_factor::=`Length of a formal proof`/`Length of a conventional proof`.
 List of 12 "real" theorems that have got formal proofs.
 Description of $HOL_light.
 Discussion of full automation and automated discovery of theorems.
 Coq::proof_assistant=http://coq.inria.fr/.
 HOL_light::proof_assistant=http://www.cl.cam.ac.uk/~jrh13/hol-light/.
 Isabelle::proof_assistant=http://isabelle.in.tum.de/.
 Mizar::proof_assistant=http://mizar.org/.
 ProofWeb::proof_assistant=http://prover.cs.ru.nl/login.php.
 QED::manifesto=http://www.cs.ru.nl/~freek/qed/qed.html.
.Close

HallChapman02
.Open HallChapman02
 Anthony Hall & Roderick Chapman
 Correctness by Construction: Developing a Commercial Secure System
 IEEE Software Magazine V19n1(Jan/Feb 2002)pp18-25
 =EXPERIENCE CORRECTNESS SECURITY FORMAL Z CSP MODEL PREDICTABLE PROCESS TOOLS COTS MXI Multos Spark Ada95 GUI C++ MSFC
 CA:="Certification Authority", Certifying smart cards.
 Process with 17 deliverables
 Handled risks by trailblazing prototypes.
 Rigorous static code checking: BoundsChecker and PC-Lint.
 Avoided unit testing as expensive and ineffective.
 Used incremental builds: many real tiny systems with tests derived from specification and automated (Rational Visual test)
 Defects introduced mainly in spec and coding.
 Coding Defects almost entirely removed in code reviews and developer testing.
 Spec errors removed in all later phases, mainly in architecture and code.
 In operation only 4 defects: 3 from coding and one from spec.  Out of 100 KLoC.
 Productivity: 28 lines of code per day.  Work: requirements 2% specification+architecture 25%, code 14%, Test 34%, fault fixing 6%, management 10% training etc 9%.
 achieved 0.04 defects per thousand line of delivered code.
.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

HamiltonZeldin76
.Open HamiltonZeldin76
 M Hamilton & S Zeldin
 Higher Order Software - A Methodology for Defining Software
 IEEE Trans SE VSE2n1(Mar 1976)pp25-32
 =DEMO METHOD HOS APOLLO CORRECTNESS FUNCTIONAL DECOMPOSITION
 Quoted as Appendix II in 
.See [Martin85].
 Compare with
.See [HamiltonHackler08]
.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

HanEtal00b
.Open HanEtal00b
 Yan Han & Liu Fengyu & Zhang Hong
 An  object-oriented model of access coontrol based on role
 ACM SIGSOFT Software Engineering notes V25n2(Mar 2000)pp64-68
 =PATTERN UML
.Close

HarrisonAvgeriouZdun07
.Open HarrisonAvgeriouZdun07
 Neil B Harrison & Paris Avgeriou & U Zdun
 Using Patterns to Capture Architectural Decisions
 IEEE Software Magazine V25n5(Jul/Aug 2007)pp38-45
 =ESSAY ARCHITECTURE PATTERNS QUALITIES TECHNIQUES REQUIREMENTS 
 Patterns provide a way of describing the trace from requirements to design. 
 p39: "Ideally, architecture documentation records decisions that architects made while designing the system"
.Close

HarrisonSnook02
.Open HarrisonSnook02
 Rachel Harrison & Colin Snook
 Practitioners Views on the Use of Formal Methods: An Industrial Survey by Structured Interview
  Information & Software Technology 43(4) : 275-283 (2001)
.See http://blue.butler.edu/~phenders/rharrison.pdf  
 =POLL EMPIRICAL UML Z B VDM CSP CCS in Marconi Prasix IBM Phillips
 Using these methods typically needs trained customers.  Most customers accept that software is error prone.
 "Some customers do not want to be tied down to what they require,"[so that they don't]"take responsibility for the systems validity".
 IBM and Praxis claim evidence of higher quality (eg fewer post-delivery failures).
 Praxis notes you get more efficient code that does less!
 No change in (traditional) life cycle but specification takes longer (and is most difficult) but reduces later effort.
 size of system is not a problem.  Understandability of the notation was not a problem. Finding useful abstractions is a problem.
 Need style as well as formal notation.  comments help.  Making implicit changes explicit helps.
.Close

HassonCooper06
.Open HassonCooper06
 Patricia Hasson & Stephen Cooper 
 A Case Study Involving the Use of Z to Aid Requirements Specification in the Software Engineering Course
 IEEE 17th conference on software engineering education and training CSEET'04 (2004)pp84-94 $CR 0606-0664 $CR 0607-0768
(In the IEEE Digital library at 
.See http://doi.ieeecomputersociety.org/10.1109/CSEE.2004.1276515
)
 =EXPERIENCE EDUCATION Z SPECIFICATION   
 When students take previous projects, done by others, and express the specs in Z the discover errors.
 Graphics and user interface details are not part of Z, tell students to omit them.  
 Need to add to the library of fundamental data types - decimals & text.
 Students need LPC first.
 (dick)|-Online copy has a non-Z font. Many symbols changed from Z Reference Manual.
.See [Spivey01]
 (dick)|- Z is the wrong language to express data formats: BNF, COBOL PICTURES, Finite state machines, etc should be used instead.
.Close

Hayes90
.Open Hayes90
 Ian Hayes
 A Generalisation of Bags in Z
 pp113-127 in Nicholls90
 =EXAMPLE Z SPECIFICATION
 physical units and bank accounts
 For set X, bags(X) ::=X<>->Integer.
.Close

Hayes93
.Open Hayes93
 Ian Hayes (ed)
 Specification Case Studies(2nd Edition)
 Prentice Hall Englewood Cliffs NJ 1993 (Series in Comp Sci)
 ISBN0-13-8325444-8 BNB92-33735 QA76.6.S667 1993(csusb)
 =TEXT SPECIFICATION Z Formal CICS Text
.Box
Contributions from Carroll Morgan, Bernard Sufrin, Bill Flinn, Ib Holm Sorensen, Roger Gimson, Steve King
Reprints: MorganSun84, Sufrin's ICL Data Dictionary(1984), Gimson&Morgan's Ease of Use paper

Specifications for: symbol table, sorting, telephone networks, unix file system, hotel room booking, Data Dictionary, Flexitime, Authentication, Time services, Reservation services, CICS and TP

Examples of: Promotion p24..., not recursive schema in p37, honesty p67, generallity and specification libraries p80, representational abstraction and procedural abstraction p147, raising questions early p190, encourages more precise use of English p208, exposes alternative readings p209, forgotten problems come up again p221


Tools: GML and syntax checker, type checker
.Close.Box
.Close

HayesJonesNichols94
.Open HayesJonesNichols94
 Ian Hayes<Ian.Hayes@cs.uq.oz.au> &  Cliff B Jones<cbj@cs.man.ac.uk> & J E Nichols
 Understanding the Differences between  VDM and Z
 ACM SIGSOFT Software Engineering Notes V19n3(Jul 1994)pp75-81
 =HISTORY FORMAL METHODS Z vs VDM
.Close

HeerBostockOgievesky10
.Open HeerBostockOgievesky10
 Jeffrey Heer & Michael Bostock & Vadim Ogievetsky
 a tour throughout the visualization zoo
 Commun ACM V53n6(Jun 2010)pp59-67 
.See http://doi.acm.org/10.1145/1743546.1743567
 =DEMO GRAPHICS HCI CS489
.Close

HelanderZhaoOhlsson98
.Open HelanderZhaoOhlsson98
 Mary E Helander & Ming Zhao & Niclas Ohlsson
 Planning Models for Software Reliability and Cost
 IEEE Trans SE V24n6(Jun 1998)pp420-434
 =THEORY COST RELIABILITY
 how to optimize reliability with fixed cost or optimize cost for a fixed reliability given hierarchy+operational profile+utilisation matrix
.Close

Hepworth90
.Open Hepworth90
 Brian Hepworth
 ZIP: a Unification Initiative for Z Standards Methods and Tools
 poster pp253-260 in 
.See [Nicholls90]
 =POSTER STANDARDS Z HISTORY forsite FUZZ ZED Genesis ZEBRA B
.Close

HildebrandtZeller00
.Open HildebrandtZeller00
 Ralf Hildebrandt & Andreas Zeller
 Simplifying Failure-Inducing Input
 Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp135-145
 =DEMO DEBUGGING TOOL Mozilla Netscape
  Given program and failure find simplest way to induce failure.
.Close

HincheyBowen99
.Open HincheyBowen99
 Michael G Hinchey & Jonathan P Bowen (Eds)
 Industrial-Strength Formal Methods in Practice
 FACIT Series of Springer-Verlag 1999 SBN 1-8533-640-4 QA76.9 F67 I53
 =EXPERIENCE FORMAL METHODS B BAN Z TABULAR ACL2 RAISE Z/EVES EVES V&V TOOL Cleanroom SSADM RSML
 for cs556/656
 Contains 
.See [BjornerGeorgePrehn99]
.See [LevesonEtal99b]
.See [KestenKleinPnueliRaanan99]
.See [BrockHunt99]
.See [LanoGoldsackSanchez99]
.See [BurrowsAbadiNeedham89]
.See [Anderson99]
.See [BernardLaffite99]
.See [BowenHinchey99]
.See [LingerTrammell99]
.See [BoralvStalmarck99]
.See [ArdisMataga99]
.See [MooreKlinkerMihelcic99]
.See [CraigenMeiselsSaaltink99]
.See [SemmensBryant99]
.See [Jacky99]
.Close

Hoare01
.Open Hoare01
 C A R Hoare
 Assertions: a personal perspective (Draft)
 Microsoft Research Ltd., Cambridge, England (6 Jun 2001)
.See 
http://research.microsoft.com/~thoare/6Jun_assertions_personal_perspective.htm
 =HISTORY ESSAY CODE ASSERTIONS INVARIANTS ALGOL60 ELLIOTT CSP Z
 Assertions as annotating designs.
 Assertions and axioms defining semantics.
 Assertions as an executable part of code.
.Close

Hoare01
.Close

Hollingsworthetal94
.Open Hollingsworthetal94
 Joseph E Holingsworth  & Sethu Sreerama & Bruce W Weide & Sergey Zhupanov
 RESOLVE Components in Ada and C++
 ACM SIGSOFT Software Engineering Notes V19n4(Oct 1994)pp40-63
 =ADVERT Resolve OBJCT-ORIENTED COMPONENTS
 See Sitaraman94
.Close

HoustonKing91
.Open HoustonKing91
 Iain Houston and Steve King
 Experiences and results from the use of Z in IBM
 CICS Project Report, pp. 588-595 in VDM Europe 91
 =EXPERIENCE Formal maintenance Z IBM CICS
.Close

HullJHart01
.Open HullJHart01
 Jonathon J Hull & Peter E Hart
 Toward Zero-Effort personal Document Management
 IEEE Computer Magazine V34n3(Mar 2001)pp30-35
 =ADVERT Save everything! Ricoh
 IM^3 := "infinite memory multi-function machine".
 copiers and printers save copy into store for indexing and retrieval.
.Close

HuntThomas02a
.Open HuntThomas02a
 Andy Hunt & Dave Thomas
 Zero-Tolerance Construction
 IEEE Software Magazine V19n5(Sep/Oct 2002)pp100-102
 =IDEA TECHNICAL QUALITY CODE MAINTENANCE EVOLUTION
 Theory (based on urban decay) that even a small unfixed defect(broken window) encourages the development of serious defects and unmaintainable software.
 So fix even the smallest problem -- or board it up and put up danger signs around it.
 Quotes XP: don't let the sun set on bad code -- fix it or throw it out.
 Quotes Scrum: have to produce a working subset in 30 days.
.Close

Ince88a
.Open Ince88a
 Darrel C Ince
 An Introduction to Discrete Mathematics and Formal System Specification
 Clarendon Press Oxford UK 1988
 =TEXT Z MATH
 Next edition reviewed
.See [Ince93]
.Close

Ince93
.Open Ince93
 Darrel C Ince
 An Introduction to Discrete Mathematics and Formal System Specification, and Z
 Oxford Univ Press NY NY 1993 ISBN 0-19-853836-7 CR9508-0570
 =TEXT Z MATH
.Box
(CR9508-0570, Berztiss)|- errors in book - treating "only if" as "iff", loosing track of units(volts expecially).
.Close.Box
.Close

ITU00
.Open ITU00
 International Telecommunications Union
 ITU Recommendation Z.100: Specification and Description Language (SDL)
 International Telecommunications Union
 =STANDARD SPECIFICATION NONSEQUENTIAL SDL MSC
SDL::="Specification and Description Language"
.Close

Jackson95c
.Open Jackson95c
 Michael Jackson(MAJ Consulting Ltd.  London) <jackson@acm.org>
 Requirements & Specifications: a Lexicon of Software Practice Principles and Prejudice
 Addison-Wesley Redwood City CA 1995 ISBN 0-201-87712-0 CR9607-0459 D.2.1
 Excerpt IEEE Software Magazine V12n6(Nov 1995)pp103-104 and
.See [Jackson94]
.Box
 No one method.
 Context diagrams/problem frames reality driven.
 Predicates for precision, composition by "and".
 Designations, definitions, assumptions.
 Moods: indicative(NAT) vs optative(REQ).
 Shared phenomena connect domains.
 Individuals.
 Danger of vagueness (especially at top level)
 Describes some risks+limits of: JSP, Z, DFDs, ERDs, top-down, hierarchies, solutions not problems.
 Ref to Phillip Kraft: "Deskilling".
 Examples: Dekker, elevators, kohnigsberg, packages, ...
 Aboricide
 Importance of critical reading
 Sent  EMail July 23rd 1996
.Close.Box
.Close

JacksonD95b
.Open JacksonD95b
 Daniel Jackson <mailto:dnj@cs.cmu.edu><http://www.cs.cmu.edu/~dnj/>
 Structuring Z specifications with Views
 ACM TOSEM V4n4(Oct 1995)pp365-389
 CR99611-0903
.Box
Frame conditions decomposition specifications
 interlocking partial specifications(partial state+some ops) with shared
ops+operations of whole are combinations of partial ops, conflicts with Z
refinement  model, needs (guard and if disclaimer then postcondition)
synchronized ops plus intersecting invariants on states, one view ND other
makes deterministic, good views are simple with complex connections, needs
implicit spec and preconditions+ explicit framing and uniform types like Z,
needs guards+ indexing+semantic actions not in Z,

Not whole+part decomposition, no master representation, no need to reconcile multplie viewpoints/perspectives
.See [ZaveJackson94]
.Close.Box
.Close

JacksonD98
.Open JacksonD98
 Daniel Jackson
 An Intermediate Design Language and its Analysis
 ACM SIGSOFT Software Engineering Notes V23n6(Nov 1998)pp121-130 & Proc 6th Int Symp on the Foundations of Software Engineering(Nov 1998)
 =DEMO NP/Nitpick Language/Tool of RELATIONS
 related to more complex Z.
 model sets as relations with a singleton range Unit:={unit}. compar 
.See [Maddux99]
 analysis by building model semantics
.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

JacksonD06
.Open JacksonD06
 Daniel Jackson 
 Dependable software by design
 Sci american V294n6(Jun 2006)pp58-65
 =SURVEY FORMAL V&V SQA CORRECTNESS MODEL CHECKING TOOLS Alloy .. Zing 
.Close

JacksonDDamon96
.Open JacksonDDamon96
 Daniel Jackson (mailto:daniel.jackson@cs.cmu.edu) & Craig A Damon(mailto: craig.damon@cs.cnu.edu)
 Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector
 Proc 1996 Int Symposium on Software Testing & Analysis(ISSTA) & ACM SIGSOFT SENotes V21n3(May 1996)pp239-249 & IEEE Trans Soft Eng VSE-22n7(Jul 1996)pp484-495
 Jackson's home page
.See http://www.cs.cmu.edu/~dnj/
.Box
V&V Z Specifications formal  Demo on style sheets for wordprocessor example. TOOL(Macintosh)Nitpick

Checks properties by enumerating possibilitis(within bounds) and displaying first counterexample.  Not animation so no constructive description of transitions but is completely automatic and can cover enormous numbers of cases by using reduction mechanisms

.Close.Box
.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

JacksonDSullivan00
.Open JacksonDSullivan00
 Daniel Jackson & Kevin Sullivan
 COM Revisited: Toll-Assisted Modeling of an Architectural Framework
 
.See [FSE8]
pp149-158
 =CASESTUDY Alloy MODEL Microsoft COM SPECIFICATION
 Uses Alloy Analyzer 
.See [JacksonD00]
 Analysis contributes to modeling by validating simplifications and spotting typographical errors rapidly and interactively. Rapid analysis encourages more daring experimental models.
 Astonished at how hard it was to preserve precise meanings when restructuring and at how useful the tool was
 Z notation may have contributed to typographical errors in previous models.
 paper+model is at
.See http://sdg.lcs.mit.edu/~dnj/publications
.Close

JacksonDWaingold01
.Open JacksonDWaingold01
 Daniel Jackson & Allison Waingold
 Lightweight extraction of Object Models from Bytecode
 IEEE Trans Software Engineering  V27n2(Feb 2001)pp156-169 also in ICSE'99 
.See [JacksonDWaingold99]
 =DEMO TOOL TECHNICAL Java bytecode MODEL Alloy Womble Superwomble Rose
 * := zero or more, ? := zero or one, ! := exactly one.   ---|-> := static.
 Womble::=http://sdg.lcs.edu/womble.
.Close

JacksonKLavi93
.Open JacksonKLavi93
 Ken Jackson & Jonah Z Lavi
 "CBSE Task Force seeks standard conceptual models for new discipline"
 IEEE Computer magazine V26n5(May 1993)pp98-99
 =CFP
 CBSE::="Computer-Based Systems Engineering"
.Close

Jacky95
.Open Jacky95
 Jonathon Jacky
 Specifying a Safety-Critical Control System in Z
 IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp99-106 CR9605-0354 D.2.1
.Box
p105: "We have already found the formal texts to be useful as descriptive documentation.  We hope that their brevity will help us build an econmical implementation.  The possiblity that they might also support safety amalyses and formal development of the implementation is an additional bonus".

p105: "User attempt operations that are interlocked... Users may select operations in any sequence they wish, subject only to the sequencing constraints imposed by the preconditions.  There is no 'flow of control'".
Interlock Preconditions
Some safety conditions need special treament because they depend on variables(sensor inputs) that are inputs and so not under constraint - and so not constrained in a precondion (or post-condition).

Op=Safe_Op or Invariant(System).
Safe_Op::= Dangerous_Op and Pre_Safe_Condition_for_Op.
Pre_Safe_Condition_for_Op::= for some State'( Dangerous_Op & Invariant(Sensors)).
For S, Invariant(S) ::=(S'=S).
Notice that Invariant(Sensors) do not appear directly in the Ops, only
inconjunction with them, and then hidden in a quantifier.

May need to add extra interlocks on transitions that are not in raw requirements.

Did not need an OO version of Z.  Defined classes of components all sharing a common schmer and separted by their identifiying names.

Useful Idioms: promotion, multiple comp ops,
.Close.Box
.Close

Jacky99
.Open Jacky99
 Jonathon Jacky
 Lessons from the Formal Development of a radiation therapy machine control program
 In 
.See [HincheyBowen99]
pp185-205
 =EXPERIENCE  Z tools TABULAR CSR SMV TMC radiation therapy machine
 formal methods can help create novel designs and original code not just post hoc.
 A detailed informal specification checked by users and designers must come first.
 Creating formal description requires design judgment.
 All documentation require much revision: content, correctness, clarity, organization.
 It is harder to do a useful formal description than a subset of the whole.  educated developers can easily do small specifications.
 Good implementation is not easy.
 Inspection and paper-and-pencil can detect most but not all errors in large Z... if modularized.
 Minor errors don't make a document useless.
.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

Jingetal95
.Open Jingetal95
 Ying Jing & He Zhijun & Wu Zhaohui & Li Jiangyun & Fan Weicheng & Xu Zhaohui
 A Methodology for High-level Software specification Construction(MHSC)
 ACM SIGSOFT Software Engineering Notes V20n2(Apr 1995)pp48-54
.Box
part of Ying Jing Ph D
acquire requirements; describe interaction;decompose;construct components, define dynamics and statics, make design model and processing.
multidimensional unified executable specs!

automated or computer aided transform abstract into concrete
graphical facilities
.Close.Box
.Close

JohnsonEtal05
.Open JohnsonEtal05
 Philip M Johnson & Hongbin Kou & Michael Palding  & Qin Zhang  & Aaron Kagawa  & Takuya Yamashita
 Improving Software development management through  Software project Telemetry
 IEEE Software Magazine V22n3(Jul/Aug 2005)pp76-85 
 =DEMO TOOL METRICS AUTOMATION DISPLAY Hackystat 
 Hackystat ::= http://hackystat.ics.hawaii.edu/. 
.Close

JohnsonSanders90
.Open JohnsonSanders90
 Michael Johnson & Paul Sanders
 From Z Specifications To Functional Implementations
 pp86-112 in Nicholls90
 Optimisation QUALITY Technical Miranda FD..FP
.Close

JuanTsaiMurataZhou01
.Open JuanTsaiMurataZhou01
 Eric Y T Juan & Jeffery J P Tsai & Tadao Murata & Yi Zhou
 Reduction METHODS for REAL-Time systems using delay time petri nets
 IEEE Trans Software Engineering  V27n5(May 2001)pp422-448
 =THEORY PETRI GRAPHIC NONSEQUENTIAL MODEL =DEMO TOOL
 DTPN::="Delay time Petri nets", have time ranges on arrows as well transitions.
.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

Keuffel03
.Open Keuffel03
 Warren Keuffel 
 The Matrix, Redux
 Software Development Magazine V11n1(Jan 2003)p56
 =REVIEW ARCHITECTURE Zachman DATA PURPOSES WEB/NET USER EUE Visual Vocabulary
 Zachman::=http://www.zifa.com/.
 EUE::="The Elements of User Experience",
.Seeee http://www.jjg.net/ia/elements.pdf
 Visual_Vocabulary::=http://www.jjg.net/ia/visvocab/.
.Close

KimWhiteheadZhang08
.Open KimWhiteheadZhang08
 Sunghun Kim & James Whitehead Jr & Yi Zhang 
 Clasifying software changes: Clean or Buggy
 IEEE Trans Software Engineering  V34n2(Mar/Apr 2008)pp181-196
 =STATISTICS OPEN SOURCE CHANGES SVM  
 Has a definition of a buggy change -- 
a change that is later changed and described as a bug/fix etc.
 Analyses a dozen open source projects.
 Doesn't find a simple way to recognise a change that contains a bug vs a clean change.
.Close

KingHammondChapmanPryor00
.Open KingHammondChapmanPryor00
 Steve King & Jonathon Hammond & Rod Chapman & Andy Pryor
 Is proof more cost-effective than testing?
 IEEE Trans Software Engineering  V26n8(Aug 2000)pp673-797
 =EXPERIENCE FORMAL COST TEST Z SPARK Ada SHOLIS helicopter TOOLs
 More faults fond per day trying to prove Z specs than by testing or inspections.
.Close

KlosterZellweger87
.Open KlosterZellweger87
 Gregory V Kloster & Andres Zellweger
 Engineering the Man-Machine Interface for Air Traffic Control
 IEEE Computer Magazine V20n2 (Feb 1987)pp47-62
 =EXPERIENCE USER REQUIREMENTS JAD GUI SREM SCENARIOS FAA AAS
 FAA AAS rigorous USER REQUIREMENTS JAD workstudy SREM SCENARIOS focus on linguistic model of GUI
.Close

Knee06
.Open Knee06
 Michael Knee 
 Computer science and computing: a guide to the literature
 Libraries Unlimited Westport CT 2006 ISBN 1-59158-160-5 Z5640.K56  QA78 Z6244 
 =SURVEY  
 A place for students to start a literature survey... where to look to find
out what has been published on computing.
.Close

Kock00
.Open Kock00
 Ned Kock
 Benefits for virtual organizations from Distributed Groups
 Commun ACM V43n11(Nov 2000)pp107-112
 =EXPERIENCE 38 PROCESS IMPROVEMENT (PI) TEAMS NET BPR TQM
 PI := conceptualPI; practicalPI.
 conceptualPI :=identification; analysis; rededign.
 practicalPI := implementation; routinization.
 Brazil and New Zealand 1993-1996 conferencing messaging.
 Iniative and leadership is bottom-up when incremental changes are made compared to   face-to-face. radical change still needs high level leadership.
 Messages are not just chat, they are part of the record.
 Groups finish faster and meet more often  than face-to-face.
 Costs are reduced vs  face-to-face.
 Results are just as good if not better than  face-to-face - you think more.
.Close

KoruZhangEmamLiu09
.Open KoruZhangEmamLiu09
 A Guneg Koru & Dongsong Zhang & Khaled El Emam & Hongfang Liu
 An Investigation into the Functional Form of the size-defect relationship for software modules 
 IEEE Trans Sofware Engineering V35n2(Mar/Apr 2009)p293-304
 =EMPIRICAL STATISTICS OPEN SOURCE LOGS DEFECTS MODULE SIZE Cox
 Problems with conventional analysis -- deleted modules, size changes, ...
 Proposes and fits Cox proportional hazards models to CVS data from Mozilla, Cn3d, JBoss, and Eclipse
 Discovers more changes are made to small modules than might be expected.
.Close

Kotze98
.Open Kotze98
 Paula Kotz'e
 Why the Hypermedia  Model is inadequate for Computer-Based Instruction
 ACM SICSE Conf Proc 6th Annual Conf on the Teching of Computing SIGCSE Bulletin V30n3(Sep 1998)pp148-152
 =THEORY FORMAL Z WWw
.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

KuncakLamZeeRinard06
.Open KuncakLamZeeRinard06
 Victor Kuncak & Patrick Lam & Karen Zee & Martin C Rinard 
 Modular Pluggable Analysis for Data Structure Consistency
 IEEE Computer Magazine  V39n12(Dec 2006)pp988-1005  
 =DEMO TOOL Hob MODULAR PROVING REALITY SETS RELATIONS ABSTRACTION PALE Bohn Isabelle flag ADTs Minesweeper httpd etc 
 Shows that the theories of ADTs from the 80s are the basis for a set of tools.
 Modules have three parts:  implementation, specification, and abstraction.  
 The code inside modules is proved to support certain assertions expressed in the language of set theory. The abstraction section defines higher level formulas using sets and the calculus of relations -- like Alloy.
 Programs are proved using the higher-level properties.
 Page 989. "One somewhat unusual feature of these abstract properties is that are outward looking: the capture important features of the system that are directly meaning ful to the users.
.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

LanoBreuer90
.Open LanoBreuer90
 K Lano &  P T Breuer
 From Programs to Z Specifications
 pp46-70 in Nicholls90
 =THEORY REVERSE ENGINEER CODE Z
.Box
reverse engineering, prime operator, monads, anti-weakest precondition, relational composition, fixed point theory, normal form, all programs reducible to Z specification, UNIFORM, DFD loop semantics
.Close.Box
.Close

LanoHaughton94
.Open LanoHaughton94
 Kevin Lano & Howard Haughton
 Object-oriented specification case studies
 Prentice Hall Englewood Cliffs NJ 1994 ISBN0-13-097015-8
 =DEMOS FORMAL MooZ OOZE/FOOPS VDM++ Z++ Object-Z Fresco OOSD OMT SSADM
.Close

Latteier01
.Open Latteier01
 Amos Latteier
 The Insider's Guide to Zope
 Software Development Magazine V9n5(May 2001)pp31+33-36
 =REVIEW TOOL OPENSOURCE WEB  Object-Oriented DATABASE ORB PYTHON
.Close

LauWang07
.Open LauWang07
 Kung-Kiu Lau & Zheng Wang  
 Software Component Models
 IEEE Trans Software Engineering  V33n10(Oct 2007)pp709-724 $CR 0812-1198
 =SURVEY MODULES ARCHITECTURE EJB COM .NET CORBA PECOS UML2.0 SOFA ...  
.Close

LeeZachary95
.Open LeeZachary95
 Arthur H Lee & Joseph L Zachary
 Reflections on Metaprogramming
 IEEE Trans Soft Eng VSE21n10(Oct 1995)pp883-893
 =THEORY metaprogramming promising but metaobject protocol a problem
.Close

LiHarmanHierons07
.Open LiHarmanHierons07
 Zheng Li & Mark Harman & Robert M Hierons 
 Search Algorithms for Regression Test Case Prioritization
 IEEE Trans Software Engineering  V33n4(Apr 2007)pp225-237 
 =EXPERIMENTS OPTIMIZATION GREEDY GENETIC HILL-CLIMBING   
 Test Case Prioritization:=following
.Net
	Tests::given.
	PT:= 1..|Tests| --- Tests, permutations.
	award : PT >-> Real = given.
	T:PT = goal.
	|- (optimal) : for all T':PT~{T}( award(T)>=award(T') ).
.Close.Net
 Greedy worked quiet well in both small and large test sets.
 Hill Climbing produced a wide range of local optima -- multimodality. Note: the hill climbing step was a single interchange of the first test in the order with another test.
.Close

Lichteretal95
.Open Lichteretal95
 Horst Lichter & Matthias schneider-Hufschmidt & Heinz Zullighoven
 Prototyping in Industrial software Projects - Bridging the Gap between Theory and Practice
 IEEE Trans SE VSE-20n11(Nov 1994)pp825-831
 =EXPERIENCE PROTOTYPING
.Box
Classifies different kinds of prototypes including Breadboards

selected 5 industrial projects with separate users and developers, with explicit planned prototyping.

Interviews during and after...

1 success, 1 pilot ok, 2 abandonned, 1 never used.

Descriptions of problems and successes.

Important to know the questions that a prototype is going to answer.

p830: "The evolutionary adaption of existing information processing infrastructures to the changing needs of their organisation, and thereby a need for a more experience-based and evolutionary strategy[...]"

Adopting prototypes with bad technical qualiies cn be dsastrous.

p831: "the central problem to be solved is the difference between application knowledge and information processing knowledge.  This gap is clearly visible at the gap between application-specific and the resulting software architecture."
.Close.Box
.Close

Lipkin99
.Open Lipkin99
  Berenice S Lipkin
  LaTeX for Linux: A Vade Mecum
 Springer Z 253.4.L38L56 1999 ISBN 0-387-98708-8
 =MANUAL LaTeX
.Close

LippertEtal03
.Open LippertEtal03
 Martin Lippert & Petra Beck-Pechau & Jorn Koch & Andreas Kornstadt & Stefan Roock & Axel Schmolitzky & Henning Wolf & Heinz Zullighoven
 developing complex Projects using XP with Extensions
 IEEE Computer Magazine V36n6(Jun 2003)pp67-73
 =EXPERIENCE AGILE XP one-size IT-workplace-solutions
.Close

LiskovZilles75
.Open LiskovZilles75
 Barbara Liskov & ?? Zilles
 Specification techniques for data abstraction
 IEEE trans on Software Eng SE-1 1 (Mar 1975) pp7-19
 =THEORY ADTs
.Close

LittlewoodWright07
.Open LittlewoodWright07
 Bev Littlewood & David Wright 
 The Use of Multilegged Arguments to increase confidence in safety claims for software-Based Systems: A Study based on a BBN Analysis of an idealized example
 IEEE Trans Software Engineering  V33n5(May 2007)pp347-365 
 =EXAMPLE THEORY RELIABILITY RISKS Arguments BAYES PROBABILITY BBN CAUSALITY SPECIFICATION CORRECTNESS TESTING  
 When should two different arguments for the safety of a system increase our belief that a system is safe?
 Answer: when the arguments do not depend (too much) on a common source of defects.
 Compare with the simpler
.See [Littlewood00]
example.
 Example BBN:=following,
.Net
 Z: random_variable(Bit)= `specification is correct`
 O: random_variable(Bit)= `test oracle is correct`
 S: random_variable(Beta_distribution(0,1,...)) = `probability of failure on demand`.
 T: random_variable(Bit)= `probability of failure during testing`.
 V: random_variable(Bit)= `formal verification proves correctness`.
 C: random_variable(Bit) = `Claim that system is fit for use should be accepted`.

Dependencies:= (Z+>O | Z+>S | Z+>V | O+>T | S+> T | S+>V | T+>C | V+>C ).

Example dependency: the correctness of the oracle O depends on the correctness of the specification (Z).

Example dependency: the parameters of the distribution of S depend on whether the specification is correct(Z).

In general, for each dependency XY+>W tabulate for each X&Y value the probability of each W value given the XY values. If W is a continuous random variable then tabulate the probability density functions. 
The table is called a
.Key conditional probability table.
See paper for a large example.

 A BBN implicitly defines a set of Conditional_independencies.

Example Conditional_independencies:= following,
.Table Independent    0f    Given
.Row O    S V     Z
.Row T    Z V    O S
.Row C    O S Z    V T
.Close.Table
So: if Z is given then O is independent of S and V.

CI::BBN=conditionally_independent, two events are independent under certain conditions.
conditionally_independent(A,B,C)::BBN= ( Pr(A B C)  = Pr(A|C) Pr(B|C) Pr(C) ).
 ...

 Bayes's formula allows us to calculate the  distribution of S and C given that  T and V are true, see $Bayes_theorem.
.Close.Net
.Close

LiuEtAl12
.Open LiuEtAl12
  Hui Liu & Zhiyi Ma & Weizhong Shao & Zhendong Niu
  Schedule of Bad Smell Detection and Resolution: A new way to save effort
  IEEE Trans on Software Eng VSE-38n1(Jan/Feb 2012)pp220-235
  =THEORY REFACTORING TECHNICAL CODE IMPROVEMENT SMELLS METHOD
  Proposes an efficient sequence for finding and fixing smelly code.
  Sells::={duplicated_code, long_method, large_class, long_parameter_list, feature_envy, useless_field, useless_method, useless_class} | $primitive_obsession,
  primitive_obsession::={simple_primitive_obsession, simple_type_code, complex_type_code}.
  sequence expressesd as "do _ before _".
  Figure 8 as a table
.Table Do before    Do after
.Row useless_class   useless_method
.Row useless_method   duplicate_code, useless_field
.Row duplicate_code    feature_envy, simple_primitive_obsession, complex_type_code, simple_type_code
.Row feature_envy, simple_primitive_obsession, complex_type_code   long_method
.Row long_method, simple_type_code   large class
.Row large_class    long_parameter_list
.Close.Table
.Close

LiuStork00
.Open LiuStork00
 Ziming Liu & David G Stork
 Is Paperless Really More
 Commun ACM V43n11(Nov 2000)pp94-97
 =ESSAY TECHNOLOGY
 Several refs to statistics and data.
 Technology is only a part of a social-material complex.
 New technology does not destroy the old. They stimulate a synergy between old and new.
 Paper is easier to move, organize, read,  annotate, and copy across platforms.
 Documents have long lives so need paper.
 Paper consumption is increasing, photocopying decreasing.
.Close

LuqiZhangBerzinsQiao04
.Open LuqiZhangBerzinsQiao04
 Luqi & Lin Zhang & Valdis Berzins  & Ying Qiao
 Documentation driven development complex real-time systems
 IEEE Trans Software Engineering  V30n12(Dec 2004)pp936-952
 =DEMO TOOL CAPS-PC AUTOMATE DOCUMENTATION REQUIREMENTS DESIGN CODE TIMING FSA/STD CARA AGILE STAKEHOLDERS LATTICES METRICS
 DDD ::= "Documentation Driven Development".
 Central dynamic data base with automatic translation between requirements, architecture, and components plus translations and executable prototypes for stakeholders.
 Process management. Risk assessment. metrics: requirements volatility, organization efficiency, product complexity, technology maturity (temperature) , ...
 CARA blood pressure maintenance IV for army stretcher.
.Close

Maguire94
.Open Maguire94
 Steve Maguire
 Debugging the Development Process
 Microsoft Press Redmond 1994
 =ADVERT MICROSOFT MS-PROCESS
 read Zachary93 as an antedote
.Close

MahonyDong00
.Open MahonyDong00
 Brendan Mahony & Jin Song Dong
 Timed Communicating Object Z
 IEEE Trans Softw Eng V26n2(Feb 2000)pp150-177
 =ADVERT LANGUAGE SPECIFICATION OBJECT-ORIENTED TIMING Z CSP TCOZ
.Close

MahoneyHayes92
.Open MahoneyHayes92
 Brendan P Mahoney &  Ian J Hayes
 A Case-Study in Timed Refinement: A Mine Pump
 IEEE Trans SE-V18 n9 (Sep 1992)pp817-826
 =DEMO Z continuous time units
 Specification_statement::= variables":" "[" Assumptions "," Guaranteed"]".

FSM NOT!

p824, Conclusions:
"The use of continuous observables, as opposed to the simple adoption of 
analog models, helps direct the the specifier away from detailed 
considerations of the method by which a system must evolve through 
time[...]leads to an algorithmic and evolutionary description of a system 
not always appropriate to the highest levels of the development process".
.Close

MaimonHorowitz99
.Open MaimonHorowitz99
 Oded Z Maimon & Roni Horowitz
 Sufficent conditions for inventive solutions
 IEEE Trans Sys Man Cybernetics V29n3(Aug 1999)pp349-361
 =EXPERIMENT POLL DESIGN
 Theory: if qualitive change and closed world then inventive.
.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

MalikZhang09
.Open MalikZhang09
 Sharad Malik & Lintao Zhang
 Boolean Satisfiabiliy -- From Theoretical Hardness to Practical Success
 Commun ACM V52n8(Aug 2009)pp76-82 
.See http://doi.acm.org/10.1145/1536616.1536637
 =SURVEY THEORY BIGO EXAMPLE PRACTICE CNF DPLL ALGORITHMS PERFORMANCE BENCHMARKS NP  COMPLEXITY PERFORMANCE 
 Theory calculates the worst case performance. 
 SAT solvers rely on the typical case (in a given domain) is not the worst case.
 The Davis Putnam Logeman Loveland algorithm with optimizations gives a usable tool. 
 See
.See [Fortnow09] 
for the theory.
.Close

MannZ06
.Open MannZ06
 Zoltan Adam Mann 
 Three Public Enemies: Cut, Copy, and Paste
 IEEE Computer Magazine  V39n7(Jul 2006)pp31-39
 =HARMFUL LOW-LEVEL CODE EDITING 
 Standard editting operations don't distinguish the half-a-dozen different purposes of using cut, copy and/or paste.
 Paste does not record the possible link between old and new.
Then a future change that should be done in several places is done once.
 Worse it does not distinguish between "copy (and keep identical)" from "copy (and then change)".
 Proposes introducing higher level operations (for complex dynamic artifacts).
.Box note
 (DRY)|-Repetitive edits indicate the need for refactoring.
.Close.Box
.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

MannaWaldinger92
.Open MannaWaldinger92
 Zohar Manna & Richard Waldinger
 Fundamentals of Program Synthesis
 IEEE Trans SE-18 n8(Aug 1992)pp674-704 CR9311-0864
 =THEORY SYNTHESIS
.Box
Similar to MannaWaldinger85.

Slowsort by Traugott Page 699, O(2^n).

Compare slowsort O(n^3) Julstrom92 - SIGSCE Bulletin V24n3(Sep 1992)pp11-13.
.Close.Box
.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

McDermid89
.Open McDermid89
 John A McDermid(Ed)
 The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems
 Butterworths London UK 1989 QA7676 D47T48 1989 ISBN 0-408-03981 BNB 89-22172 Dewy 005.1
 =WORKSHOP FORMAL TOP-DOWN Z VDM REQUIREMENTS
.Box
state of research into theory of Top-down methods, practice with formal refinement

Refinement guided by non-functional issues: p4, 189,

non-functional requirements by R Macdonald & C Sennett pp122-133

Problems with editor for VDM (McDermid89 p207)

 p136 specification is a mixture of formal text and natural language text
Chapter 6, Z specification is a set of states, an initial state and some relations on the set of states [McDermid89]

Contents
 Forward: two obstacles: modularization and refinement
 John A McDermid Intro pp1-12
Alan Dix & Michael Harrison pp12-26.p14 Design of editor determined by QT(screen vs line)
 Cliff B Jones pp79-89. History of refinement in VDL, VDM ...Operation decomposition(pre,post), ADTs, Reification (MAJackson)
 Steve King & Ib Holm Sorenson, pp90-121 Library: requirements,spec( abstract state, operations),  design(states, invariants, operations, algorithm). proof oblgations. experienced designers "just know" how to implement a spec.
 Ruaridh Macdonald & Chris Sennett pp122-133. security (and safety) properties require special refinement. Some functions can be partly incorrect and extra properties have to be proved.
 Dave Neilson pp134..161. pp150 oo-refinement (finite approximation)
 John B  Wordsworth Program construction sort pp179-190. formal requires guidance by human and is pushed by nonfunctional pressures.
 JCP Woodcock & B Dickinson pp191-217. Proof rules. Problems with editting(p207)
.Close.Box
.Close

McLellanEtal98
.Open McLellanEtal98
 Sam McLellan & Al Roesler & Zongming Fei & Savita Chandran & Clay Spinuzzi
 Experience Using Web-Based Shotgun Measure for Large-System Characterization and Improvement
 IEEE Trans Soft Eng V24n4(Apr 1998)pp268-277
 =EXPERIENCE =TOOL DATA Mining in Software 
 Answering one query generates more new types of queries
.Close

MendesAl-FakhriLuxton-Reilly06
.Open MendesAl-FakhriLuxton-Reilly06
 Emilia Mendes & Lubna Al-Fakhri & Andrew Luxton-Reilly (New Zealand)
 A Replicated Experiment of Pair-programming in a 2nd-year software development and design computer science class
 ACM SIGCSE Bulletin V38n3(Sep 2006) & proc ITiCSE 2006 pp108-112 
 =EXPERIMENT REPLICATION SUEVEY PEDAGOGY PAIR-PROGRAMMING JAVA DATABASE PATTERNS  
 Repeats experiment reported in last ITiCSE 2005 by same authors.
 Pair programming in ungraded labs.
 Pair programming significantly linked to better examination scores, passing rate, and quality of independent (solo?) work.
 10% students hated it, 50% liked it, 15% liked it a lot.
 Literature survey of 20 items.
.Close

MenziesGreenwaldFrank07
.Open MenziesGreenwaldFrank07
 Tim Menzies & Jeremy Greenwald & Art Frank 
 Data Mining Static Code Attributes to Learn Defect Predictors
 IEEE Trans Software Engineering  V33n1(Jan 2007)pp2-12 + discussion
V33n9(Sep 2007)pp637-640
 =EXPERIMENT DATA MINING NASA MODULES DEFECTS METRICS Halsted McCabe Lines of Code
 Don't measure predictive power on the sample used to train the data mining formula. Instead train on a largesub sample and test on the rest -- the holdout subsample.  
 Brittleness: The best formula for  some popular forms of data mining depends on the training subsample chosen. 
 A Bayesian `learner`  is less brittle and can predict defective modules correcly 70% of the time and falsely predict defects in ok modules 25% of the time.
 Discussion with Hongyu Zhang and Xiuzhen Zhang in V33n9.
.Close

MernicEtal99
.Open MernicEtal99
 Marjan Mernic & Viljem Zumer & Mitja Lenic & Enis Avdicausevic
 Implementation of multiple attribute grammar inheritance in the tool LISA
 SIGPLAN Notices V34n6(Jun 1999)pp68-75
 =ADVERT LANGUAGE TOOL GRAMMAR INHERITANCE OBJECT-ORIENTED JAVA
.Close

MichalewiczFogel00
.Open MichalewiczFogel00
 Zbigniew Michalewicz & David B Fogel
 How to solve it: modern hehuristics
 Springer Verlag NY 2000 ISBN 3-540-66061-5 CR0102-0057 I.2.8QA63.M53
 =EXAMPLES MATHS ALGORITHMS TSP SAT OPTIMISATION
 Real problems do not appear in chapters.  You need to think.
 How to mathc problems to algorithmic solutions and how to tune algorithms to specific problems.
 Little computer science! 
 Dangerously addictive for some people.  
.Close

Milicev07
.Open Milicev07
 Dragan Milicev
 On the Semantics of Associations and Association Ends in UML
 IEEE Trans Software Engineering  V33n4(Apr 2007)pp238-251 
 =THEORY SEMANTICS UML ASSOCIATION {unique} {nonunique} Z  
 Notes an ambiguity in the UML 2.0 standard metamodel of associations ("the restrictive")
and proposes a fix("the intensional").
 Very bdetailed and Precise using Z.
.Close

MillerStrooper04
.Open MillerStrooper04
 Tim Miller & Paul Strooper
 A Framework and Tool Support for the Systematic Testing of Model-Based Specifications 
 ACM TOSEM Trans Software Eng & Methodology V12n4(Oct 2003)pp409-439
 =CASESTUDIES TOOL MODEL CHECKING Z-like Sum SPECIFICATIONS Possum CONSTRAINT-SOLVING SETS RELATIONSHIPS MUTATION
.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

Monin03
.Open Monin03
 Jean-Francois Monin
 Understanding Formal Methods Springer Verlag London UK 2003 ISBN 1-85233-247-6 QA76.6 M6513
 =SURVEY FORMAL CTL Z B VDM LP HOL CCS CSP LCF LTL PVS TLA
.Close

MurugappanKeeni03
.Open MurugappanKeeni03
 Mala Murugappan & Gargi Keeni
 Blending CMM and Six Sigma to meet Business Goals
 IEEE Software Magazine V20n2(Feb/Mar 2003)pp42-48
 =EXPERIENCE BUSINESS QC STATISTICS PURPOSES QUALITIES QFD IMPROVEMENT SW-CMM PROCESS
 7year process! Uncovered synergy.
 Using z scores to quantify capability.
 Roughly a 3\sigma process has 68 defective lines/KLoC but a 6\sigma process has only 3 per million LoC.
.Close

MurphyNotkinSullivan95
.Open MurphyNotkinSullivan95
 Gail C Murphy & David Notkin & Kevin Sullivan
 Software Reflexion Models: Bridging the Gap between Source and High-level Models
 
.See [Kaiser95]
pp18-28
 =DEMO EXPERIENCES MODULE REVERSE ENGINEERING Z C/C++
 understanding is an iterative process
 engineer postulates model; maps source code names to model; sees structural differences
.Close

MurphyNotkinSullivan01
.Open MurphyNotkinSullivan01
 Gail C Murphy & David Notkin & Kevin J Sullivan
 Software Reflexion Models: Bridging the Gap between Design and Implementation
 IEEE Trans Software Engineering  V27n4(Apr 2001)pp364-380
 =FORMAL+EXPERIENCE MODEL TOOL TECHNICAL CODE Z
 See 
.See [MurphyNotkinSullivan95]

.See [MurphyNotkin97]

.See [MurphyNotkin96]
 gives formal Z model of a reflexion model and its computation from code.
 Relates high level entities to source code entities.  And high level relations
to source code relations.
 extract a reflexion model of the code and iteratively make them match via maps
from model to code.
 Tool looks for mismatches.
 Experience includes MS Excel, > 1M LoC of C.
.Close

NarayanaDharap90
.Open NarayanaDharap90
  K T Narayana & S Dharap
  Formal Specification of a Look Manager
  IEEE Trans Software Engineering SE-V16n9(Sep 1990)pp1089-1103
 =DEMO Z FORMAL SPECIFICATION GRAPHIC USER INTERFACE GUI
.Close

Nicholls90
.Open Nicholls90
 J E Nicholls(Ed)
 Z users Workshop: Oxford 1989
 British Computer Society/Springer VerlagWorkshops in Computing Series (WiCS) 1990 ZUM'89
 =SURVEY FORMAL Z
 List of 55 companies and universities using Z
 ZUM'95 will be published in Springer-Verlag LNCS
.Close

NeilMEtal98
.Open NeilMEtal98
 Martin Neil & Gary Ostrolenk & Mary Tobin & Mark Southworth
 Lessons from Using Z to Specify a Software Tool
 IEEE Trans Soft Eng V24n1(Jan 1998)pp15-23
 =EXPERIENCE Z SPECIFICATIONS caused problems
 high productivity+low fault density inexplicable
 (dick)|- wot no DDD!
.Close

NentwichEtal00
.Open NentwichEtal00
 Christian Nentwich & Wolfgang Emmmerich & Anthony Finkelstein & Andrea Zisman
 BOX: Browsing objects in XML
 Software - Practice & Experience V30n15(Dec 2000)pp1661-1676
 =DEMO WWW/NET UML XML XMI DOM VML Java DHTML JavaScript
.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

NuseibehZave10
.Open NuseibehZave10
 Bashar Nuseibeh & Pamela Zave
 Software Requirments and designs: the work of Michael Jackson
 Good Friends Publishing Co, NJ 2010
 =SURVEY REQUIREMENTS DESIGN JSD JSP 
 Help....
.Hole NuseibehZave10
.Close

ObrenovicStarcevic04
.Open ObrenovicStarcevic04
 Zeljko Obrenovic & Dusan Starcevic
 Modeling multi-modal human-computer interaction
 IEEE Computer Magazine  V37n9(Sep 2004)pp65-72
 =IDEA MODEL HCI UML
.Close

Ogdenetal94
.Open Ogdenetal94
 William F Ogden & Murali Sitaraman & Bruce W Weide & Stuart H Zweben
 The RESOLVE Framework and Discipline - A Research Synopsis
 ACM SIGSOFT Software Engineering Notes V19n4(Oct 1994)pp23-28  See 
.See [Sitaraman94]
 =ADVERT RESOLVE LANGUAGE Framework Discipline
.Box
Framework+language+discipline
 Two kinds of components: abstract/specifications/concepts vs concrete realisations.
concepts implemented by realizations, contexts
 realisations use concepts (not other realizations)
 realisations have two parts: additional concepts + body
 highly parameterized/generic/templates -> instances

Key Target: To be able to prove a generic implementation of a concept once and for all - once proved in general all valid instanciations will be correct.

.Close.Box
(dick)|-Problem:  Too damn complex(IMHO)
.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

ORegan06
.Open ORegan06
 Gerard O'Regan
 Mathematical Approaches to Software Quality
 Springer-Verlag Secaucus NJ 2006 ISBN 184628242X CR 0710-0962
 =UNREAD MATHEMATICS Z Vienna Hoare Dijkstra Parnas UML
.Close

Ortiz07
.Open Ortiz07
 Sixto Ortiz Jr 
 Getting on ZBoard the Enterprise Service Bus
 IEEE Computer Magazine  V40n4(Apr 2007)pp15-17   
 =ADVERT ESB SERVICES ARCHITECTURE GLUE SOA INTEGRATION LEGACY EAI   
 EAI::="Enterprise Application Integration", hub and spoke. Adaptors. Brokers. Pipelines. Point-to-Point
 SOA:="Service Oriented Architectures",XML defined WEB communication, SOAP HTTP UDDI ...
 Hub and spoke can have performance problems.
 ESB::="Enterprise Service Bus", analogy hardware bus, handles locating servers, adapting data, routing messages. JCA | SAP IDoc. Many protocols...
 Does more work .... So larger servers.
 Many rival products.
.Close

Palshikar01
.Open Palshikar01
 Girish Keshav Palshikar
 Applying Formal Specifications to Real-World Software Development
 IEEE Software Magazine V18n6(Nov/Dec 2001)pp89-97
 =ADVICE FORMAL SPECIFICATION METHODS Z MATH
.Box
 Define role of math in your process: purpose, scope, value,+ change management.+ validation + how used
 define steps
 split purpose, quality, interfaces, behavior, USECASES.
 focus math on right parts of application to
 choose notations and tools to match requirement type
 maintain abstraction: avoid design decisions and implementation detail
 avoid partial, over- and under-specification.
 modular specs with  natural/good structure
 Select best representations from many candidates
 reuse metaphors and patterns
 be true to the spirit of the notation.
 Review and test specs.  Note test cases.
 document and explain.
 effectively use tools
 state/prove/discuss/argue about/demonstrate all properties.
.Close.Box
.Close

ParameswaranEtAl07
.Open ParameswaranEtAl07
 Manoj Parameswaran & Xia Zhao & Andrew B Whinston & Fang Fang 
 Reengineering the Internet for better security
 IEEE Computer Magazine  V40n1(Jan 2007)pp40-44     
 =IDEA CERTIFIED PROVIDERS pay for sending SPAM MALWARE ...
.Close

ParikhZvegintzov82
.Open ParikhZvegintzov82
 G Parikh & ?? Zvegintzov
 Software Maintenance
 IEEE Tutorial IEEE Computer Society Order No 453
 =TUTORIAL MAINTENANCE EVOLUTION engineering lifecycle
.Close

Pascal94
.Open Pascal94
 G Zachary Pascal/G Pascal Zachary??
 Showstopper! The Breakneck Race to Create Windows NT and the Next Generation at Microsoft
 Free Press 1994 (ref from Keuffel95b Software Development Magazine(Aug 1995))
 =EXPERIENCE MS-PROCESS Windows
 
.See [Zachary93]
.Close

PauloMasieroOliveira99
.Open PauloMasieroOliveira99
 Fabiano B Paulo & Paulo C Masiero & Maria C F de Oliveira
 Hypercharts: Extended Statecharts to Support Hypermedia Specification
 IEEE Trans SE V25n1(Jan/Feb 1999)pp33-49
 =THEORY Z multimedia
 Timed transitions and history notation
.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

PfleegerHatton97
.Open PfleegerHatton97
 Shari Lawrence Pfleeger & Les Hatton
 Investigating the Influence of Formal Methods
 IEEE Computer Magazine V30n2(Feb 1997)pp33-43 + letter from N Zvegintzov IEEE Computer Magazine V30n4(Apr 1997)p6
 =analysis PRAXIS CDIS system CDM CCS FSM effect on CODE quality:
 project achieved unusually low faults per LOC and testable and simple code. 
 Data collection incomplete and confused hence stops comparison of methods
 Quote from reply to Zvegintzov:"reading may be far more effective for discovering certain kinds of faults than testing is."
.Close

PflegingZetlin06
.Open PflegingZetlin06
 Bill Pleging & Minda Zetlin
 The Geek Gap: Why business and technology professionas don't understand each other and why they need each other to survive.
 Prometheus Books Amherst MA 2006 ISBN 1591024135
 =UNREAD =ANECDOTAL Information Technology CSCI372 GEEK SUIT 
.Close

Polack01
.Open Polack01
 Fiona Polack
 A Case Study using Lightweight formalism to Review an Information System Specification
 Software - Practice & Experience V31n8(10 Jul 2001)pp757-780
 =CASESTUDY V&V SPECIFICATION SAZ Z SSADM Ordnance Survey UK
 Lightweight formal review can detect many problems: unmet requirements, inconsistencies, contradictions, ambiguity, ...
 Original documents generated 100page Z+text +questions review.
 Uncovered missing constraints, ambiguities, conflicts, inconsistencies, ...
.Close

PolackWhistonMander93
.Open PolackWhistonMander93
 F Polack & M Whiston & K Mander
 The SAZ project: Integrating SSADM and Z
.See [WoodcockLarson93] pp541-557
.See [BourdeauCheng95] (ref)
 =THEORY Z SSADM
.Close

PopovStriginiMayKuball03
.Open PopovStriginiMayKuball03
 Peter Popov & Lorenzo Strigini & John May & Silke Kuball
 Estimating Bounds on the reliability of Diverse systems
 IEEE Trans Software Engineering  V29n4(Apr 2003)pp345-359
 =THEORY RELIABILITY MULTI-VERSION REDUNDANT CONTROL SYSTEM
 If a piece of software is deterministic it either fails or works on each different input data -- with fixed 1 or zero probability.
 However can work with the probability of a data set occurring that leads to failure,
  Hence probability joint failure depends on the correlation of the failure probabilities of failure of the components.
  Much statistics and some small testing.
.Close

PostonBruen87
.Open PostonBruen87
 Robert M Poston  & Mark W Bruen
 Counting Down to Zero Software Failures
 IEEE Software V4n5(Sep 1987)pp54-61
 =EXPERIENCE SQA RISKS engineering
.Close

Potteretal91
.Open Potteretal91
 Ben Potter & Jane Sinclair & David Till
 An Introduction to Formal Specification and Z
 Prentice Hall Hemel Mempstead UK 1991
 Review IEEE Software Mar 1993 pp113-114"Undergraduate Text" + CR 9304-0183
 =TEXT FORMAL SPECIFICATION Z
.Close

RallisLansdowne01
.Open RallisLansdowne01
 Nancy E Rallis & Zachary F Lansdowne 
 Reliability Estimation for a Software System with Sequential Independent Reviews
 IEEE Trans Software Engineering  V27n12(Dec  2001)pp1057-1061
 =MATHEMATICS RELIABILITY TEST/FIX Bayesian
 review:=test; correct.
 |- If the number of faults in a system is distributed in a Poison distribution before review then after review and fixing it has a new Poison distribution with mean multiplied by (1-(the detection rate)).
.Close

Ramaswamy00
.Open Ramaswamy00
 Ramkumar Ramaswamy
 Latency in distributed, sequential application designs
 ACM SIGSOFT Software Engineering notes V25n2(Mar 2000)pp51-55
 =IDEA DESIGN WEB/NET PERFORMANCE
 adjust user interface to separate network services with user input.
 MADE:=`Maximal Anticipation, Deferred Execution`.
 coalesce as many services into one request as possible so long as they are all normally required,  reversible, require no new user data, response  times are met, and zt least one service has to bemade now.
.Close

Rannetal94
.Open Rannetal94
 D Rann & J Turner & J Whitworth
 Z: A beginner's guide
 Chapman & Hall 1994
 =TEXT SPECIFICATION Z
.Close

RiceSeidman94
.Open RiceSeidman94
 M D Rice & S B Seidman
 A Formal Model for Module Interconnection Languages
 IEEE Trans SE V20n1(Jan 1994)pp88-101
 =THEORY MILs Z FORMAL Specification  STYLE Conic
 MILs::="Module Interconnection Languages".
 Selecting, Connecting, Checking legallity of connections, creating template from structure
.Close

RomanWilcox94
.Open RomanWilcox94
 Gruia-Catalan Roman & C Donald Wilcox
 Architecture-Directed Refinement
 IEEE Trans SE-30n4(Apr 1994)pp239-258
 =DEMO Swarm Formal Program vs specification  concurrent
 PurposeQuality->(Tech)->System
.Box
Focussed on program derivation from spec (by creative but verifiable steps)
Description of formal process on p239
.List
  formal treatment
  Better Understanding of the fundamental issues
  development of tools
.Close.List
Ignores Feijs93

Ignores formal methods for specs: Z, VDM, ... "Current program derivation methods simply exclude considerations regarding target architecture from the formal framework"!?!

Shows that Swarm/UNITY can discuss architectural constraints
.Close.Box
.Close

Roojimansetal96
.Open Roojimansetal96
 Jan Roojimans & Hans Aerts & Michiel van Genuchten
 Software Quality in Consumer Electronic Products
 IEEE Software Magazine V13n1(Jan 1996)pp55-71
 =EXPERIENCE QUALITY ECONOMICS
 Claims that goal must be for zero defects - 100k shipped on day one and must work
 Sudden growth in project size made estimates go badly wrong along with sudden increase in communication caused test defects
.Close

RossakEtal97
.Open RossakEtal97
 Wilhelm Rossak & Vassilka & Leon Jololian & Harold Lawson & Tamar Zemel
 A Generic Model for Software Architectures
 IEEE Software Magazine V14n4(Jul/Aug 1997)pp84-92
 =ADVERT ECBS GENSIF GENERIC COMPONENT 
 ECBS:=Engineering of Computer-Based Systems.
 GenSIF GENERIC systems integration Framework.
  BB:=Biulding blocks in clusters characterized by interfaces with contracts used in scenarios.
.Close

Ross05
.Open Ross05
 Philip E Ross
 The Exterminators
 IEEE Spectrum Magazine (Sep 2005)pp36-
 =ADVERT Praxis MATH Z  Spark PROTOTYPES V&V TOOLS TESTING MONDEX
 Company demonstrates that by getting very clear and reliable requirements
expressed mathematically and using a reliable language to write the code 
you can reduce the number of faults to 1 for 25KLoC on project with 
200KLoC.
.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

SafayiniEtAl08
.Open SafayiniEtAl08
 Frank Safayini & P Robert Duimering & Kimberley Zheng & Natalia Derbentseva & Christopher Poile & Bing Ran 
 Requirements Engineering in New Product Development
 Commun ACM V51n3(Mar 2008)pp77-82
 =CASESTUDY COMPANY INTERACTION COMMUNICATION REQUIREMENTS SAP   
 Company divided by functions with outsourced software development.  Requirement Engineers separated from Market Sponsors by a Feasibility Analyst.
 Requirement Engineers had helpful knowledge but had a weakness with coordination.
 Requirement Engineers found less help especially with coordination, knowledge, and communication.
 In terms of functions, REs were helped by the software developers.  The project manager and feasibility analysts and operations were helped by the REs.
 Examples: when Market Sponsors change requirements halfway thru a project the REs see it as unhelpful,.... In reverse, MS finds RE jargon unhelpful.
 Article includes proposals. Notes that reorganization would be a good idea that would not fly.
 (dick)|- Sounds like the company Dilbert works for. 
The lists of unhelpful behaviors should be studied by practitioners.
No reference to Yourdon's analysis of Market vs Engineering speech.
No discussion of possible technologies.
.Close

SamadzadehZand95
.Open SamadzadehZand95
 Mansur Samazadeh & Mansour Zand(eds)
 Proceedings of the Symposium on Software Reusability (SSR'95)
 ACM SIGSOFT Software Eng Notes Special Issue(Aug 1995)
 =PROCEEDSING REUSE SSR 1995
 April 1995 Seatle Washington USA

.See [Griss95]
.See [Prieto-Diaz95]
.See [ShawM95]
Tracz95b
.See [Arango95]
.See [Batoryetal95]
.See [GennariAltmanMusen95]
.See [AlencarCowanLucenaNova95]
.See [CaplanHarandi95]
.See [PoulinWerkman95]
.See [FranceHorton95]
.See [Wasmund95]
.See [FraserLeishmanMcLellan95]
.See [Gomaa95]
.See [BiemanKang95]
.See [BiemanZhao95]
.Close

SchulmeyerMcManus92
.Open SchulmeyerMcManus92
 G Gordon Schulmeyer & James I McManus(eds)
 Total Quality Management for Software
 Van Nostrand Reinhold NY NY 1992 ISBN 0-422-00794-9  QA76.76.Q35T67
 =HOWTO TQM QUALITY SQA
.Box
contibuting Authors: Rick Bridges, Emanual R Baker, Lois Zells, Ken Mendis, G Gordon Schulmeyer, Ron S Kenett, David R Carey, Don Freeman, James I Holden, Anthony F Shumskas Donald J Reifer, James H Dobbins, Richard Zultner, Herb Krasner, D. Paul Smith, Dennis A Christenson, Alfred J Lamperez, Stell T Huang, Robert G Mays, Barba B Affourtit, Harlan D Mills!
.Close.Box
.Close

SemmensBryant99
.Open SemmensBryant99
 Lesley Semmens & Tony Bryant
 Rigorous Review Technique
 In 
.See [HincheyBowen99]
pp231-254
 =DEMO EXPERIENCE METHODS Z SSADM TELSTAR BT( British telecom) FORMAL SQA STRUCTURE  ANALYSIS DESIGN DFD ER DATA RRT
 RRT::="Rigorous Review Technique".
 How to use Z to check structured method outputs.
 It is easier to teach simplified Z mathematics to analysts than to teach a mathematically competent an understanding of analytical skills.
.Close

SenguptaBhattacharya09
.Open SenguptaBhattacharya09
 S Sengupta & S Bhattacharya
 Formalization of UML use case diagram - a Z notation based approach
 Computing & Informatics, 2006. ICOCI '06. International Conference on... .(6-8 June 2006) pp 1 - 6 
 =DEMO FORMALIZATION USE CASES Z ERD 
 Proposes a Z + ERD  model of a set of use cases with relations between them. 
 Their model is not normalized and is comparatively trivial. 
.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

ShawB75
.Open ShawB75
 B Shaw (ed)
 Formal Aspects of Computer Science
 Joint IBM University of Newcastle upon Tyne Seminar 3rd-6th Sep 74
 =PROCEEDINGS FORMAL
 Papers by Bekic Hoare Hopcroft Rabin Scott Winograd Zemanek.
 Hoare(p17) joke on ugly goto vs decent abortion
 efficiency and termination related.
 H Zemanek on history(p180) "We may not realise but a blue-print is a formal definition of the object to be produced..."
 Cunningham (p209) use of regular algebras to model algorithms via Kleene Sequence [Backhouse & Carre??]
.Close

ShawMetal95
.Open ShawMetal95
 Mary Shaw & Robert DeLine & Daniel V Klein & Theodore L Ross & David M Ross & Gregory Zelesnik
 Abstractions for Software Architecture and Tools to support them
 IEEE Trans on Software Eng VSE-21n4(Apr 1995)pp314-315 
.See [CR]
9602-0120 D.2.1
 =DEMO ARCHITECTURE SET? DFD TIMING
.Close

Sheppard95
.Open Sheppard95
 D.Sheppard
 An introduction to formal specification with Z and VDM
 McGraw Hill International Series in Software Engineering 1995
 =TEXT Z VDM SPECIFICATION
.Close

Shirky08
.Open Shirky08
 Clay Shirky 
 Here comes everybody
 Penguin NY NY 2008 HM851 S5465 ISBN 978-1-59420-153-0
 =EXAMPLES SOCIOLOGY WEB/NET ECONOMICS SOCIAL CAPITAL SMALL WORLDS POWER LAWS
 Net lowers cost of communication, publication, copying, collaboration  to ZERO.  So a lot more of all of these.
 More is Different.  Faster is Different.
 New paradigm: Publish; Filter.
 Many attempts, failure is free, on the way to one big success.
 A shared resource needs motivated people and people need Face-to-face meetings.
 Developing_a_resource::= Promise; Tool; Bargain.
 Examples: Usenet FlashMobs F/OSS Linux SourceForge Flickr MySpace FaceBook MeetMe EBay Wikipedia Wikitorial Encarta
 Also see short article
.See [Shirky03]
.Close

Simmons06
.Open Simmons06
 Erik Simmons 
 The Usage Model: Describing Product usage during design and development
 IEEE Software Magazine V23n3(May/Jun 2006)pp34-41 
 =SYNTHESIS REALITY USER PURPOSE SCENARIO PERSONAS REQUIREMENTS 
 Puts together many different kinds of usage modeling techniques into a 3 tier framework -- Figure 1.
 Describes three types of product drivers: Business, Technology, and Usage.  Good products fit all of these.  Usage defines the connection between technology and business.
 Distinguishes goals (I don't want to feel stupid) from features (intuitive HCI) and tasks(add an X to a Y).
 Three tiers: Supporting data + Overview + usage details.
.List
 Supporting data: personas, demographics, use conditions, ethnographic data.
 Overview: Road-map, storyboards, concept and context diagrams, user experience landing zone.
 Details: use cases, scenarios, user task flows, operational profiles.
.List
 Road-map: shows how usage is expected to evolve.
 User experience landing zone:  Table -- each row shows, an area plus the "outstanding", "target", and "minimum"  degrees of user experience.
.Close.List
.Close.List
.Close

Sitaraman94
.Open Sitaraman94
 Murali Sitaraman(coordinator)
 Special Feature: Component-Based Software Using RESOLVE
 ACM SIGSOFT Software Engineering Notes V19n4(Oct 1994)pp21-67
 =PAPERS COMPONENTS RESOLVE
.Box
Collection of papers:
 I. Framework and Discipline:
 Ogdenetal94, William F Ogden & Murali Sitaraman & Bruce W Weide & Stuart H Zweben
 II. Specifying Components:
Edwardsetal94, Stephen H Edwards & Wayne D Heym & Timothy J Long & Murali Sitaraman & Bruce W Weide
 III. Implementing Components:
Buccietal94, Paolo Bucci & Joseph E Holingsworth & Joan Krone & Bruce W Weide
 IV. Ada and C++:
Hollingsworthetal94, Joseph E Holingsworth & Sethu Sreerama & Bruce W Weide & Sergey Zhupanov
 V. Bibliography:
Edwards94, Stephen H Edwards
 Authors:
Paolo Bucci, Stephen H Edwards, Wayne D Heym, Joseph E Holingsworth, Joan Krone, Timothy J Long, William F Ogden, Sethu Sreerama, Murali Sitaraman, Bruce W Weide, Sergey Zhupanov, Stuart H Zweben
.Close.Box
.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

SnookButler06
.Open SnookButler06
 Colin Snook & Michael Butler 
 UML-B: Formal modeling and design aided by UML
 ACM TOSEM Trans Software Eng & Methodology V15n1(Jan 2006)pp92-122 
 =EXPERIENCE MATHEMATICAL Z B SPECIFICATION GRAPHIC UML  TOOLO U2B
TRANSLATOR 
 Idea: To help practitioners understand B use UML.
  Tried Class diagrams and state machines. 
 B Machines shown as package containing class diagram and a table of operations, guards, and
actions in B.   
 Associations appear as relations and maps like in Z.
 \mu-B = micro-B for actions and constraints.
 UML-B profile. Includes create, delete, and subroutine stereotypes. Plus some tagged values.
 Specialization/generalization models  refinement in B.
 State machines mappedto B machines with "SELECT..., THEN...".
 page 114: Proposes an alternative mathematical model of state machines. 
For each state in machine define a set of objects:  the objects currently in that state.
 (dick)|-This was in 
.See [Weinberg75].
.Close

SowaZachman92
.Open SowaZachman92
 John F Sowa & John A Zachman
 Extending and Formalizing the Framework for Information Systems Architecture
 IBM Systems Journal V31n3(1992)pp590-616
 =ADVERT METHOD ERDS MODELS 
 data><function><network><people, ends-means model,
 time-model Frameworks,
 ambiguous semantic nets (conceptual graphs) with ambiguous quantification
.Close

SpewakHill93
.Open SpewakHill93
 Steven H Spewak & Steven C Hill
 Enterprise Architecture Planning: Developing a blueprint for data applications and technology
 QED Information Sciences Inc Wellesley MA 1993 ISBN 0-89435-436-1 
.See [CR]
9309-0651
 =COOKBOOK ERD VALUE ARCHITECTURE EAP Zachman
.Box Review
EAP = Enterprise Architecture Planning
 Zachman framework
 Not design, highlevel managerial and interpersonal
 Michael Porter Value aided chain (Competitive advantage, Free Press NY NY)
 Entity-relationship model
.Close.Box
.Close

Spivey88
.Open Spivey88
 JM Spivey
 Understanding Z:A Specification language and its Formal Semantics
 Cambridge Tracts on Theoretical Computer Science 1988 Cambridge U press UK
 =THESIS Z SPECIFICATION SEMANTICS circular
.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

Spivey90
.Open Spivey90
 J. Michael Spivey
 Specifying a Real-Time Kernel
 IEEE Software V7n5(sep 1990)
 =DEMO Z TIMING SPECIFICATION
.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

SpiveySufrin90
.Open SpiveySufrin90
 J M Spivey & B A Sufrin
 Type Inference in Z
 pp6-31 in Nicholls90
 =THEORY TOOL generic polymorphic typechecker
.Close

StankovicZhang02
.Open StankovicZhang02
 A Distributed Parallel Programming Framework
 Nenad Stankovic & Kang Zhang
 IEEE Trans Software Engineering  V28n5(May  2002)pp478-493
 =ADVERT VISUAL TOOL NONSEQUENTIAL FRAMEWORK Java
.Close

Stecher93
.Open Stecher93
 Peter Stecher(IBM Eurocoordination)
 Building Business and Application Systems with Retail Application Achitecture
 IBM Sys Journal V32n2(1993)pp278-306
 =ADVERT RAA generic architectures
 RAA provides generic architectures for various industries that can be customized to a particular case. Uses Zachman87
.Close

Stein92
.Open Stein92
 Richard Marlon Stein
 Safety by Formal Design
 BYTE V17n8(Aug 1992)p157
 =ARTICLE refers to Z but no details
.Close

Stepneyetal92
.Open Stepneyetal92
 Susan Stepney & Rosalind Barden & David Cooper
 Object Orientation in Z
 Springer Verlag 1992
 =MONOGRAPH OBJECT-ORIENTATION Z
.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

SullivanSochaMarchukov97
.Open SullivanSochaMarchukov97
 Kevin J Sullivan & John Socha & Mark Marchukov
 Using Formal Methods to Reason about Architectural Standards
.See [ICSE'97]
 =EXPERIENCE Z MICROSOFT COM ARCHITECTURE SUCCESS
 Analysed MS COM and averted an architectural disaster
.Close

SunDong06
.Open SunDong06
 Jun Sun & Jin Song Dong
 Design Synthesis from Interaction and State-Based Specification
 IEEE Trans Software Engineering V32n6(Jun 2006)pp349-364
 =DEMO SCENARIO MESSAGE SEQUENCE CHARTS LCS Z AUTOMATION PVS Java CSP
 Shows that it is possible to synthesize correct code from specifications
using universal live sequence charts plus Z (Zed) state pre/postconditions.
 Introduces idea of a package of Z specifications.
 Design is a set of cooperating sequential processes to reduce state
explosion. 
.Close

Swaine00?
.Open Swaine00?
 Michael Swaine
 All Those Zombies
 Dr. Dobbs #317(Oct 2000)pp117-120
 =HISTORY PC TECHNICAL 1980-2000
.Close

ThayerDorfman90
.Open ThayerDorfman90
 Richard H Thayer & Merlin Dorfman(eds)
 System and Software Requirements Engineering
 IEEE CS Press Tutorial Cat No.EH0304-6 QA76.758 S87
 =TEXT BOOK n-squared, std decision tables decision trees pdl statecharts rnet sdl petri net sa dfds era ooa ssadm jsd descartes(JE Urban's DDD), STARTS Z srem psa/psl glossary(pp605-676), bibliography(pp677-695) case studies(553-603)
.Close

Thomas92
.Open Thomas92
 Martin Thomas
 Limits and Customers are Driving Change (Insider dept)
 IEEE Software V9n2(Mar 1992)p10
 =ARTICLE FORMAL METHODS STANDARDS VDM Z REQUIREMENTS OUTSOURCED TECHNICAL
 "Software Engineering is emerging as a true engineeering discipline
with structures + standards+ ethics + attitudes similar to traditional engineering.
 This accounts for the growing use of mathematical formal development methods such as VDM and Z.
 These methods are proving to be suitable for a wide range of projects
particularly for requirements capture and analysis and high-level design.
 [...] split between architects and builders[...]subcontracting to developers in low-wage third-world countries."
.Close

ThomasBostromGouge07
.Open ThomasBostromGouge07
 Dominick M Thomas & Robert P Bostrom & Marianne Gouge 
 Making Knowledge Work in Virtual Teams
 Commun ACM V50n11(Nov 2007)pp85-90
 =POLL 13 MANAGERS 30 PROJECTS DISTRIBUTED TEAMS COMMUNICATION TECHNOLOGY MATHODS 
 ICT::="Information and Communication Technologies".
 More than 20 different ICTs.
 It is not enough to make technology available.
 Problems: team volatility, time pressue, interoperability all lead to work stopages and managerial intervention.
 All teams used audio confeences, EMail, and the phone.
 >70% used: Fax, project management, calendar, IDEs,many-to-many chat, versioning, instant 1-1 messaging,...
 Intervention:=(opportunity | problem) triggers leader actions and changes; aim for higher participation and capacity, leading to project outcomes.
 May have to shut down an ineffective technology as well as promote a better one.
 Triggers: outside the team, inadequate tools, breakdown of trust and relationships, interference in group work, member knowledge.
 Interference:turnover, cultural difference, physical distance, time zones
.Close

TianRudrarajuLi04
.Open TianRudrarajuLi04
 Jeff Tian & Sunita Rudraraju & Zhao Li
 Evaluating Web Software Reliability Based on Workload and Failure Data Extracted from Server Logs
 IEEE Trans Software Engineering  V30n11(Nov 2004)pp754-769
 =EXPERIENCE WEB/NET RELIABILITY WORKLOAD LOGGING DATA STATISTICS SMU/SEAS KDE
 Access logs provide evidence of problems in content: "permission denied" and "file does not exist".
  Errors consistent with a Poisson process with time varying parameters,
  Can measure the growth in reliability.
  (Goel-Okumoto model):  expected_number_of_errors(time) = N*(1-exp(-b*time)) for some N and b.
  Similar models of work load for two different web sites: weekly cycle.
  Similar reliability models.
  What measures workload? Bytes served, hits, users, sessions?
.Close

Tristram03
.Open Tristram03
 Clair Tristram
 Extreme Programming: The Zero G experience (Sidebar)
 MIT Technology Review V106n9(Nov 2003)pp38-39
 =EXPERIENCE XP InstallAnywhere
.Close

TsaiEtAl08
.Open TsaiEtAl08
 W T Tsai & Xinyu Zhou & Yinong Chen & Xiaoying Bai
 On testing and evaluating service-oriented software
 =CASESTUDY SOA SERVICES TESTING CRM
 IEEE Computer Magazine V41n8(Aug 2008)pp40-46 
 Using statistical analysis to select tests.
 Can test many services in parallel.
 CRM::="Coverage relationship model", Tsai et al in 2007.
.Close

VitharanaZahediJain03
.Open VitharanaZahediJain03
 Padmal Vitharana & Fatemah "Mariam" Zahedi & Hemant Jain
 Design, retrieval, and Assembly in component-based Software Development
 Commun ACM V46n11(Nov 2003)pp97-102
 =ADVERT DOMAIN REALITY  Object-Oriented MODULES QUALITIES REUSE CBSD
 Distinguishes management goals (cost effectiveness, ease of assembly, customization, reusability, maintainability) from technical qualities(coupling, cohesion, number of components, size, complexity).
.Close

Warms01
.Open Warms01
 Tom M Warms
 Tracing the Execution of C++ Programs
 ACM SIGCSE Bulletin V33n4(Dec 2000)pp64-67
 =HOWTO TECHNICAL EDUCATION TRACE C++
  Simpler than Zelkowitz's trace tables.  
  All variables for a function in one column, appearing each time value changed.
 Record Return addresses to handle many calls.
  underline input values.  Italicize output.
  Draw line between assumed values and derived ones.
  Function names on top of line, conditions break line.
 On exit make explicit value of function = returned value.
.Close

WilliamsEtal00
.Open WilliamsEtal00
 Laurie Williams & Robert R Kessler & Ward Cunningham & Ron Jeffries
 Strengthening the Case for Pair Programming
 IEEE Software Magazine V17n3(Jul/Aug 2000)pp19-25
 =SURVEY EXPPERIMENT POLL EXPRRIENCE TECNICAL ORGANISATION XP PEOPLE
 initially pair programming reduces productivity(work/people) 60% but later it is 15% lower, meanwhile defects drop to close to zero and time to complete drops 40..50%.
 programmers engjoy pair ptogramming.
 some problems if one partner has too much or too little ego,
.Close

WojcikWojcik91
.Open WojcikWojcik91
 Zbigniew M Wojcik & Barbara E Wojcik
 Rough Grammar for Efficient and Fault-tolerant Computing on a Distributed System
 IEEE Trans SE-V17n7(Jul 1991)pp652-668
 =DEMO DDD NON_SEQUENTIAL SCHEDULING GRAMMARS
 If algorithm -> production grammar then grammar can be used for task allocation to nodes in a distributed system.
.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

Woodcock06
.Open Woodcock06
 Jim C P Woodcock 
 First steps in the verilied software grand challenge
 IEEE Computer Magazine  V39n10(Oct 2006)pp57-64
 =DEMO PROVING SOFTWARE REPOSITORY TOOLS EXAMPLE SPECIFICATION PROOFS Mondex SECURITY MICROSOFT SDV  Z Z/Eves Alloy Event-B OCL Raise KIV ASMs Perfect developer PVS VERIFICATION
 15 year worldwide project.  
 See
.See http://qpq.csl.sri.com/
.See http://vstte.ethz.ch
.Close

WoodcockDavies9x
.Open WoodcockDavies9x
 J.C.P.Woodcock & J.Davies
 Using Z: specification
 Prentice Hall International Series in Computer Science 1995? (In preparation)
 =DEMO proof refinement specification Z
.Close

WoodcockLoomes88
.Open WoodcockLoomes88
 Jim Woodcock & M Loomes
 Software Engineering Mathematics
 Pitman London UK 1988
 =HANDBOOK MATHEMATICS formal Z Reality
.Close

WoodK93
.Open WoodK93
 Kenneth R Wood
 A practical approach to software engineering using Z and the refinement calculus
.See [Notkin93] pp 79-88
 =DEMO Z REFINEMENT
.Box
 methodology, need for smooth path
 codified discrete mathematics of Z + data encapsulation of refinement calculus.
 NOT Refinement calculus developed within Z(a thesis+a techrport at PRG)
 NOT just Morgan's calculus 
.See [MorganC90]
 Specification statement: frame:[O(pre, )post] with x0,y0,...

BUT
 Formal path from design to implementation without new notations or unnecessary transformations.
 Language R^Z - Z schemata define types, specs define operations etc.

 Drop Z "Trappings" and use within refinement calculus

Examples: a text editor, a diary

 p81: operation is robust if it defines a total relation.
 p82. Complex operation with elegant Z specs can lead to confusion. R^Z
specs look more like programs but are at the same lvel of abstraction and
rigor...."Softw engineers put off by more abstruse notations."
 PROC name ( L( (VALUE|RESULT|...) arg:type),";" ) \defeq spec.

 p83-4: Promotion. Operation defined at higher level can define a more refined operation in Z.
 p84-85: In R^Z Scema's are types so no schema inclusion. Instead more
refined operations explicitly handle componets in subschema. Hence name
duplication is ok...scoped ids in R^Z.

 p86(Conclusion) : Discusses problem of proof in engineering. States effect
of proof is to improve the confidence of the engineer. States "need to find
suitable notations which both appeal to practitioners and possess the
expressive and calculational power required to specify and develop complex
systems."

Frame problems:
.See [Borgidaetal95]
, 
.See [BicarreguiRitchie95]

.Close.Box
.Close

Wordsworth93
.Open Wordsworth93
 John B Wordsworth
 Software Development with Z: A Practical Approach to Formal Methods
 Addison-Wesley Redwood City CA 1992
 =TEXTBOOK MATHEMATICAL SPECIFICATION Z
.Close

Wu04
.Open Wu04
 Fangjun Wu 
 Empirical Analysis of Entropy distance Metric for UML Class Diagrams
 ACM SIGSOFT Software Engineering Notes V29n5(Sep 2004)p35
.See http://doi.acm.org/10.1145/1022494.1022524
 =EMPIRICAL UML METRIC Zhou banking understanding
 Abstract: "[...]we provide empirical evidence for supporting the role of the structure complexity metrics for UML class diagrams, specifically Zhou's metric. Our results, based on data related with bank information system, indicate that the metric is basically consistent with human beings' intuitions. "
.Close

XiaodongEtal98
.Open XiaodongEtal98
 Yuan Xiaodong & Hu Deqiang & Li Yong & Zheng Guoliang
 COOZ: A Complete Object-Oriented Extension to Z
 ACM SIGSOFT Software Engineering Notes V23n4(Jul 1998)pp76-81
 =IDEA OBJECT-ORIENTED Z COOZ
 super/subtypes + <post> if <pre>
.Close

YangJiang07
.Open YangJiang07
 Zhihui Yang & Michael Jiang 
 Using Eclipse as a tool-integration platform for software development
 IEEE Software Magazine V24n2(Mar/Apr 2007)pp87-89      
 =ADVERT TOOL Eclipse  GMF EFM JDT WTP TPTP JUnit OPEN SOURCE
 Claims Eclipse supports Soup to Nuts development (requirements to testing).
 Claims Eclipse has 23 languages, 1,385 plugins, and support for Java, C/C++, etc.
 Lists resources on page 89.
 Problems discovering, understanding and managing plugins and updates.
 Before developing a plugin: choose the level of integration (page 89) and review the resources
.Close

YipEtAl09
.Open YipEtAl09
 Alexander Yip & Xi Wang & Nickolai Zeldovich & M. Frans Kaashoek
 Improving Application Security with Data Flow Assertions
 MIT Computer Science and Artificial Intelligence Laboratory
.See http://people.csail.mit.edu/nickolai/papers/yip-resin.pdf
 =REPORT LANGUAGE Resin SECURITY DATAFLOW ASSERTIONS PHP Python WWW/Net
 33% runtime penalty to monitor flows of data and block SQL-injection attacks 
and unauthorised sending of passwords, for example.
.Close

YuSchatz03
.Open YuSchatz03
 Haiping Yu & Sol M Schatz
 A Framework for Model-Based Design of agent-Oriented Software
 IEEE Trans Software Engineering  V29n1(Jan 2003)pp15-30
 =THEORY AGENT PETRI INHERITANCE NONSEQUENTIAL CTL MODEL CHECKING TOOL INA UML
 Petri nets model agent behavior.
  INA::TOOL="integrated Net Analyzer", Roch & Starke Humboldt-Universitat zu Berlin, inst fur Informatic
.Close

Zachary93
.Open Zachary93
 G Pascal Zachary
 Climbing the Peak: Agony and Ecstacy of 200 Code Writers Beget Windows NT
 Wall Street Journal (May 26 1993), review mentions it p106 IEEE Software magazine Sep 1995
 =ARTICLE Microsoft Windows NT MS process
.Close

Zachman87
.Open Zachman87
 John A Zachman
 A Framework for Information Systems Architecture
 IBM Systems Journal V26n3(1987)pp276-292
 =ADVERT METHOD ARCHITECTURE
 (what><How><where><when><why><who), architects drawings, Figure 2 Framework: data,process, network vs scope, business model, infor system vs designers view, Details, different people mean different things by architetcture(p291)

Method used in SpewakHill93,...
.Close

ZachosMaidenTosar05
.Open ZachosMaidenTosar05
 Konstantinos Zachos & Neil Maiden & Amit Tosar
 Rich-Media Scenarios for discovering Requirements
 IEEE Software Magazine V22n5(Sep/Oct 2005)pp89-97
 =DEMO TOOL  WEB Requirements TEXT  Scenarios + Video Audio BLOBs ART-SCENE DMAN ATC
 Figure 2. UML metamodel
 ART-SCENE generates What-if alternatives  to given normal scenario steps.
 ART-SCENE 3 layer architecture.
.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

Zahniser94
.Open Zahniser94
 Richard A Zahniser<70313.1325@compuserve.com>
 Design By Walking Arround(DBWA)
 Comm ACM V36n9(Sep 1993)pp115-123
 =ADVERT DBWA Method non-sequential DFDs ERAs Objects
 highly concurrent blitz 7 or 8 views using storyboarding (brainstorm on blackboard?) team work 30 deliverables
 Months of work done in weeks.
.Close

ZagalAhuesVoehl02
.Open ZagalAhuesVoehl02
 Jose Pablo Zagal & Rauk Santelices Ahues & Miguel Nussbaum Voehl
 Maintenance-Oriented Design and Development: A Case Study
 IEEE Software Magazine V19n4(Jul/Aug 2002)pp100-106
 =CASESTUDY PROCESS LIFECYCLE MAINTENANCE GAMES EMBEDDED ARCHITECTURE TOOLS
 proposes a process/lifecycle where maintenance is the 3rd phase.
 Maintenance_Oriented_Design_and_Development ::= Base_design; Maintenance.
Implementation is a special part of maintenance.
 Developing hand-held video games with educational content.
 Claims the process reduced  costs throughout process.
.Close

ZambonelliJenningsWoolridge04
.Open ZambonelliJenningsWoolridge04
 Franco Zambonelli & Nicholas R Jennings & Michael Woolridge
 Developing Multiagent Systems: The Gaia Methodology
 ACM TOSEM Trans Software Eng & Methodology V12n3(Jul 2003)pp317-370
 =CASESTUDY IDEAS MODELLING  AGENT ORGANISATION METHOD GAIA
 Agents:: Autonomous & Situated & Proactive & Social. Abstractions: Environment; Roles & Interactions; Organizational Rules; Organizatio
nal Structure(patterns). Liveness  specified by regular expressions with interleaving and indefinite repeti
tion(\omega).
 Roles imply responsibilities. Forces acting on design of organization: Structure of the real world, rules, technical possibilities, and simplicity.
.Close

ZaremskiWing93
.Open ZaremskiWing93
 Amy Moorman Zaremski<amy@cs.cmu.edu> & Jeanette M. Wing<wing@cs.cmu.edu>
 Signature Matching: A Key to Reuse
 pp182-190
.See [Notkin93]
 =DEMO MATHEMATICAL specification modules LARCH
 
.See [ZaremskiWing95]

.Box
Use signatures derived from components to retrieve reusable components. Two kinds: functions and modules. Experiments with exact match and with relaxed matching flavors.  Using Standard ML. LIST QUEUE SET

modules have a multi-set signature

Flavors of relaxed matching: more general than, more special than, type unification, transforms

Complements traditional IR methods: facets[Prieto-Diaz89]
Use gnu-Emacs+mouse .: goal: easy access to programmers from a normal software development environment.... as easy as string searching.
.Close.Box
.Close

ZaremskiWing95
.Open ZaremskiWing95
 Amy Moorman Zaremski<amy@cs.cmu.edu> & Jeanette M. Wing<wing@cs.cmu.edu>
 Specification Matching of Software Components
.See [Kaiser95] pp6-17
 =MATHEMATICAL specification modules LARCH Lattice
.Close

ZaremskiWing95a
.Open ZaremskiWing95a
 Amy More Zaremski & Jeanette M. Wing
 Signature Matching: A Tool for Using Software Libraries
 ACM TOSEM V4n2(Apr 1995)pp146-170
 =MATHEMATICAL specification modules LARCH Lattice
 See
.See [ZaremskiWing93]
.Close

ZaremskiWing97
.Open ZaremskiWing97
 Amy More Zaremski<amy@cs.cmu.edu> & Jeanette M. Wing<wing@cs cmu edu>
 Specification Matching of Software Components
 ACM TOSEM V6n4(Oct 1997)pp146-170
 =MATHEMATICAL FUNCTIONs LARCH Lattice pre-post SPECIFICATION INHERITANCE
 ignoring qualities cf 
.See [ZaremskiWing95a]
.Close

ZariSaiedianNaeem01
.Open ZariSaiedianNaeem01
 Mazen Zari & Hossein Saiedian & Muhammad Naeem
 Understanding and Reducing Web delays
 IEEE Computer Magazine V34n12(Dec 2001)pp30-37
 =ANALYSIS TIMING WEB/NET LATENCY 
 Delays = Browser DNS HTTP UDP/IP TCP/IP Sockets server
 http1.1 helps.
 avoid BMP!
 remove whitespace!
.Close

Zave85
.Open Zave85
 Pamela Zave
 A Distributed Alternative to Finite-State-Machine Specifications
 ACM TOPLAS 7 1 Jan 1985 pp10-36
 =DEMO DAD JSD STD non-sequential
.Close

Zave88
.Open Zave88
 Pamela Zave
 Assessment(Session summary: 4th Int Wkshop on Software Specification & Design 1987 (IWSSD4))
 ACM SIGSOFT Software Engineering Notes v13n1 (Jan 1988)pp40-43
 =REPORT SPECIFICATION DESIGN
 also see pp197-199 of ThayerDorfman90
.Close

Zave91
.Open Zave91
 Pamela Zave
 An Insider's Evaluation of PAISLey
 IEEE Trans SE-17 n3(Mar 1991)pp212-225
 reviewed by D M Berry CR9202-0092
 =ADVERT PAISLEY Formal SPECIFICATION LANGUAGE
.Close

Zave93
.Open Zave93
 Pamela Zave<pamela@research.att.com>
 Feature Interactions and Formal Specifications in Telecommunications
 IEEE Computer Magazine( Aug 1993)pp20-28
 =DEMO FORMAL REQUIREMENTS
.Box
p22: "a general truth: Once a major evolutionary step is completely accepted and understood, specifications become clearer and simpler than when half steps were sowing confusion"

pp24-27: Ideas that help: Types and roles, Invariants(constraints on a space, and definitions), Parsing inputs to recognize significant patterns,

p26:Specifications as LPC predicates
Composing specifications.
p28:Features as 1stclass citizens. definable and manipulable

p28: Which feature now? precedence lists, message passing, exceptions

p30: "[...] general-purpose reasoning will not suffice for these challenges. We need to focus first on concepts, models, and principles that capture the essence of telecommunications and think later about how they relate to other application domains.
 Perhaps the most difficult problem of all is the incoherent, unprincipled, and ad hoc behavior of current telecommunications systems. [...] If specificers work diligently on the telecommunication domain, then principles governing all aspects of feature interaction will emerge."

.Close.Box
.Close

Zave96
.Open Zave96
 Pamela Zave<pamela@research.att.com>
 Formal Methods are Research, not development
 IEEE Computer Magazine V29N4(Apr 1996)pp26-27
 =ESSAY FORMAL METHODS
.Box
Describes sample of engineering needs.
But which modeling technique to reccommend. and none match engineers perceptions.
Finding the right FM for a domain is a research problem.

A good model: abstractions illuminate not obscure.

Example papers on callwaiting vs callforwarding and ignoring many kinds of phones. Instead: should isolate time-multiplexing into a module...

Analogies for a good FM: BNF, code optimization algorithms, protocol checking. Special attention to particular SW tools (compilers, OSs) has paid off.

Need for specialized models for different disciplines: civil, chemical,.... but Compsci tries to cover the software part of all of these.
.Close.Box
.Close

Zave97
.Open Zave97
 Pamela Zave
 Classification of Research Efforts in Requirements
 ACM Computer Surveys V29n4(Dec 1997)pp315-321
 =SURVEY REQUIREMENTS Research
.Box
Note
 first_dimension: problems_in (1:investigation+2:specification+3:evolution)

 investigation:(1.1:communication+1.2:generate strategies to meet vague goals+1.3:priorities and satisfactory ranges+1.4:allocation of requirements to resources+1.5:costs/risks/schedules+1.6: completeness
 specification:(2.1:multiple views and representations+2.2:evaluating alternatives+2.3:good_specifications(complete&consistent&unambiguous)+2.4:check specification vs requirements+2.5:fit to design and implementation)
 evolution:(3.1:reuse as system evolves+3.2:reuse in other systems+3.3:reconstructing requirements)

second_dimension:contribution (A:State of the art | B:proposed process change | C:proposed product change | D:case study applying solution to example | E:Evaluation and comparison | F:Proposal for measurement changes)

.Close.Box
.Close

Zave04
.Open Zave04
 Pamela Zave
 Address Translation in Telecommunication Features.
 ACM TOSEM Trans Software Eng & Methodology V13n1(Jan 2004)pp1-36
 =EXAMPLE TELECOMMUNICATION REQUIREMENTS IDEAL
 Valuable to abandon old messy ideas and abstract a new ideal from a large set of examples.
.Close

ZaveCheung09
.Open ZaveCheung09
 Pamela Zave & Eric Cheung
 Compositional Control of IP Media
 IEEE Trans Software Engineering V35n1(Jan/Feb 2009)pp46-66 
 =DEMONSTRATION COMPLEX DESIGN NON-SEQUENTIAL MEDIA TELEPHONY PBX SIP IMS flowLink HoldSlot 
 Usually the channels used to send media through a network are independent of the signalling channels.
 This makes it difficult to design protocols and systems that work correctly.  
 Proposes a couple of abstractions that help: flowLink and holdSlot.
.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

ZaveJackson97a
.Open ZaveJackson97a
 Pamela Zave<pamela@research.att.com> & Michael A Jackson
 Requirements for Telecommonications Services: An Attack on Complexity
 RE'97
.See [RE'97] pp106-117
 =CASE-STUDY TABULAR FSM/STD FORMAL REQUIREMENTS
 
.See [ZaveJackson96]
 effective techniques based on general principles:  define the environment not the new system + leave out unnecessary + formalize only when effecive and helpful+combine and specialize languages + parallel state decomposition + uniform event semantics with no internal events(no vars if can refer to attributes of most recent events)
.Close

ZaveJackson97b
.Open ZaveJackson97b
 Pamela Zave<pamela@research.att.com> & Michael A Jackson
 Four Dark Corners of Requirements Engineering
 ACM TOSEM V6n1(Jan 1997)pp1-30
 =ESSAY REQUIREMENTS REALITY PURPOSE
.Close

ZaveJackson98
.Open ZaveJackson98
 Pamela Zave & Michael A Jackson
 A Component-Based Approach to Telecommunication Software
 IEEE Software Magazine V18n5(Sep/Oct 1998)pp70-78
 =DEMO DFC system
 Applies the pipe-and-filter archtectural style to describing complex telecommunications systems.
.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

Zavidoviqueetal91
.Open Zavidoviqueetal91
 Bertrand Zavidovique & Veronique Serfaty & Christian Fortunel
 Mechanism to Capture and communicate Image-Processing Expertise
 IEEE Software Magazine V8n6(Nov 1991)pp37-50
 =DEMO REUSE EXPERTISE
.Close

Zdun09
.Open Zdun09
 Uwe Zdun (Guest Editor)
 Capturing Design Knowledge (Special Section)
 IEEE Software Magazine V26n2(Mar/Apr 2009)pp25-49
 =COLLECTION DESIGN TOOL METHOD ARCHITECTURE EXPERIENCE RATIONALE ARAL
 Argues that between the requirements and the software comes a number of design decisions and
that the reasoning behind them may be lost.
 Also notes that software rots if it is not looked after well.
 Titles
.List
 Capturing Design Knowledge
 Modularization of a large-scale business application -- A CAse study
 The Decision View's Role in Software Architecture Practice
 Software Architecture Design Reasoning: A case for improved Methodology Support
.Close.List
.Close

Zeeman77
.Open Zeeman77
 E C Zeeman
 Catestrophe Theory: Slected papers 1972-1977
 Addisson Wesley 1977 ISBN 0-201-09015-5 (pbk) ISBN 0-201-09014-7 QA614.58.Z42 514.7 BNB 77-21459
 =THEORY MATHEMATICS DYNAMICS CATESTROPHES TIPPING POINT DISCONTINUITIES Thom BIOLOGY SOCIOLOGY ECONOMICS EMBRIOLOGY EULER BUCKLING SHIPS STABILITY MARKETS STABILITY BOOM and BUST
 A mixture of applications and derivations of the key theorems of Rene Thom's Catestrophe theory.
 Shows how discontinuous behavior emerges in continuous systems leading to instability, 
development, boundaries, revolutions, and so on.
 Also see Rubbish Theory.
.Close

Zeler99
.Open Zeler99
 Andreas  Zeler
 Yesterday, my program worked. Today, it does not. Why?
 ESEC/FSE'99 SIGFOFT SE Notes V24n6(Nov 1999)pp253-267
 =ADVERT TOOL MAINTENANCE DELTA DEBUGGING the  GDB
.Close

Zelkowitz90
.Open Zelkowitz90
 Marvin V Zelkowitz
 A Functional Correctness Model of Program Verification
 IEEE Computer magazine V23n11(Nov 1990)pp30-39
 =DEMO Formal Functional Education Trace Tables
.Box
Trace_table::=trace_table_header #trace_table_row.
trace_table_header::="Part"><"Cond"><#variable.
trace_table_row::= statement_part><predicate><#expression.

predicates and expressions expressed in terms of initial values of variables.
.Table
.Row Part
.Item Cond
.Item x
.Item y
.Row x:=x+y
.Item true
.Item x+y
.Item y
.Row if(x>y)
.Item x+y > y
.Item "
.Item "
.Row y:=x-1
.Item true
.Item "
.Item x+y-1
.Close.Table
.Close.Box
.Close

Zeller01
.Open Zeller01
 Andreas Zeller 
 Automated Debugging: Are we close
 IEEE Computer Magazine V34n11(Nov 2001)pp26-31
 =EXPERIENCE =DEMO TOOL delta DEBUGGING MOZILLA OPEN SOURCE GUI Wynot
 delta_debugging::=http://www.st.cs.uni-sb.de/ddd/.
 Helps spot differences between circumstances that trigger the bug and those that do not. Also looks for code changes that make a difference.

 Next see 
.See [Zeller02]

.Close

Zeller02
.Open Zeller02
 Andreas Zeller 
 Isolating cause-effect chains from computer programs
 SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp1-10
 =DEMO delta DEBUGGING compare automatic TESTING HOWCOME GDB GCC
 Comparing tests that run vs tests that fail helps diagnose problems.
  Previously used different inputs.   Determines what caused the bug. 
This time tried initial stats of RAM. Helps find out why the bug happened.   Process is being patented
delta_debugging::=http://www.st.cs.uni-sb.de/dd/.
 Follows on from 
.See [Zeller01]
 AskIgor::=http://www.askigor.org/.
.Close

ZellerHildebrandt02
.Open ZellerHildebrandt02
 Andreas Zeller & Ralf Hildebrandt 
 Simplifying and Isolating Failure-Inducing Input
 IEEE Trans Software Engineering  V28n2(Feb  2002)pp183-200
 =THEORY delta debugging =DEMO MOZILLA GCC BUGS TESTS TOOL WYNOT AUTOMTION
 Theory of changes in circumstances of a run.... that may fail or may succeed. 
 A change, \delta : Run->Run.
  Circumstances include data input and command line options!
 Tool automatically searches (binary search)  out simplest test case that cause a given bug to appear, given an initial large bug report.
 See also
.See [Zeller01]
and
.See [HildebrandtZeller00]
.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

Zhang08
.Open Zhang08
 Hongyu Zhang 
 On the Distribution of Software Faults
 IEEE Trans Software Engineering  V34n2(Mar/Apr 2008)pp301-302
 =EXPERIMENT STATISTICS PROBABILITY FAULTS BUGS DEFECTS MODULES Eclipse 
 For x:[0..], Pareto(x)::= 1-(\gamma/x)**\beta.
 Weibull(x)::=1 -exp(-(x/\gamma)**\beta).
 Weibull predicts % of faults in % of modules better than Pareto in Eclipse.
.Close

ZhangBudgen12
.Open ZhangBudgen12
 Cheng Zhang & David Budgen
 What do we know about the effectiveness of software design patterns
 IEEE Trans Software Engineering  V38n5(Sep/Oct 2012)pp1213-1232
 =SURVEY EMPIRICAL RESEARCH GoF PATTERNS
 611 candidate papers, 11 experiments, 7 experiences. 
 Need more data! Focus research on fewer patterns and their impact on maintenence. 
 No support for the claimed benefits of using design patterns. 
 Some support for GoF patterns helping maintenance. 
 Some evidence they do not help novices learn about design. 
.Close

ZhangRyderLandi96
.Open ZhangRyderLandi96
 Sean Zhang & Barbara G Ryder & William Landi
 Program Decomposition for Pointer Aliasing: A Step toward Practical Analyses
 Proc 4th ACM SIGSOFT 1996 Symp on the Foundns of Software Eng: ACM SIGSEN V21n6(Nov 1996)pp81-92
 =DEMO TECHNICAL CODE POINTERS
.Close

ZhangPatel11
.Open ZhangPatel11
 Yuefeng Zhang & Shailesh Patel 
 Agile model-driven Development in practice
 IEEE Software Magazine V27n6(Mar/Apr 2011)pp84-91
 =EXPERIENCE Motorola AGILE MDD SIFT SLAP SCRUM ITERATIONS MODELS INCEMENTAL FUNCTIONS SPRINTS UML ASN iSL CODE GENERATION COMPONENTS DAILY PLAN 
 Correlates Model driven practices with agile practices.  Thus: pair modeling rather than pair programming.  Thus continuous early testing of models with tools and simulators.
 Tools generate code from models.
 The architecture, design, and code all iterate.
 Low level design starts with sequence diagrams with no data and when tested the data is added (and verified).
 1 iteration = 3 sprints.
 Monitor `sprint velocity` to detect process problem and plan corrections.
 Must automate as many steps in process as possible.
 Stream line and integrate systems engineering, design, and coding.
.Close

ZhangKim10
.Open ZhangKim10
 Hongyu Zhang & Sunghun Kim
 Monitoring software quality evolution for defects
 IEEE Software Magazine V27n4(Jul/Aug 2010)pp58-64
 =DEMO SQA STATISTICS CONTROL CHARTS  
 Good collection of patterns: trends, impulses, hills, small variations, and roller coasters.
 Misquotes the general formula for control limits.
 No mention of warning and action limits. 
.Close

ZhangXu04
.Open ZhangXu04
 Yingzhou Zhang & Baowen Xu
 A Survey of Semantic Description Frameworks for Programming Languages
 ACM SIGPLAN notices V39n3(Mar 2004)pp14-30
 =HISTORY FORMAL LANGUAGE SEMANTICS
.Close

ZhangZhangCao01
.Open ZhangZhangCao01
 Kang Zhang & Da-Quien Zhang & Jiannong Cao
 Design, Construction, and Application of a Generic Visual Language Generation Environment
 IEEE Trans Software Engineering  V27n4(Apr 2001)pp289-307
 =DEMO Object-Oriented MVC GRAPH GRAMMAR TOOL VisPro
 VPL::="Visual Programming Languages".
 Introduces Protocol into the center of the Model-View-Controller pattern
.Close

ZhaoBailey-KeloggOrdonez01
.Open ZhaoBailey-KeloggOrdonez01
 Feng Zhao & Chris Bailey-Kelogg & Ivan Ordonez
 The spatial aggregation Language
 Dr. Dobbs #323(Apr 2001)pp68+69+72-77
 =ADVERT C++ LIBRARY ENVIRONMENT SAL for distributed data analysis and control
 SAL1.2 ::=http://www.parc.xerox.com/zhao/sal.html.
.Close

ZhaoFoster99
.Open ZhaoFoster99
 Ziping Zhao & Ted Foster
 Modeling Roles with Cascade
 IEEE Software Magazine V16n5(Sep/Oct 1999)pp86-93
 =EXPERIENCE PATTERN GIS
 Cascade:=multilevel Composite,
 role_object:= { X:=X.core | X.role, has : X.core(1)-(many) X.role, X.role := a | b | c| ... }.
.Close

ZhouLeungXu09
.Open ZhouLeungXu09
  Yuming Zhou & Hareton & Baowen Xu
  Examining the Potentially confounding effect of class size on the associations between object-oriented metrics and change-proneness
  IEEE Trans Software Engineering V35n5(Sep/Oct 2009)pp607-623
  =EMPIRICAL ECLIPSE OBJECT-ORIENTED METRICS CHANGES SIZE
  Size correlated with common oo metrics and with the number of 
changes made to modules in Eclipse.
  Casts doubt on the traditional interpretation of coupling and cohesion 
as directly driving the number of changes in a class.
.Close

Zhuetal95
.Open Zhuetal95
 Jiang Zhu & Ted G Lewis & Weldon Jackson & Russell L Wilson
 Scheduling in Hard Real-Time Applications
 IEEE Software Magazine V12n3(May 1995)pp54-83
 =DEMO TIMING SCHEDULES
.Close

ZhuEtal04
.Open ZhuEtal04
 J Zhu & Z Tian & T Li  & W Sun & S Ye & W Ding & C Wang & G Wu & L Weng & S Huang & B Liu & D Chou
 Model-driven business process integrationm andmanagement: A Sae study with the bank SinoPac Regional Service Platform 
 IBM J Research & Development V48n5/6(Sep 2004)pp649-669 $CR 0605-0528
  =UNREAD =EXPERIENCE WORKFLOW MODELING BPIM BPM Model Blue 
 (Norita Ahmad)|-"...before we model anything, we must identify the stakeholders, their concerns, and their views and viewpoints..."
.Hole
.Close

ZickertBeck12
.Open ZickertBeck12
  Frank Zickert & Roman Beck
  Coping with existing systems in information systems development
  IEEE Trans Software Engineering  V38n5(Sep/Oct 2012)pp1027-1039
  =CASESTUDY FINANCIAL SYSTEMS ISD SOLUTION COMPLEXITY PATTERNS INTEGRATE EXTEND REENGINEER PROBLEM SPACE 
 Bottom-up may be better than top-down when analyzing existing systems. 
 Problem space: issues (existing vs new) requires and or inconsistent not-sufficient...
.Close

Ziemann02
.Open Ziemann02
  Paul Ziemann
  The UML Bibliography
  Retrieve from
.See http://www.db.informatik.uni-bremen.de/umlbib/
  =BIBLIOGRAPHY UML WWW
.Close

ZimmermannEtAl10
.Open ZimmermannEtAl10
 Thomas Zimmermann & Rahul Premraj & Nicolas Bettenburg & Sascha Just & Adrian Schroter & Cathrin Weiss
 What makes a good bug Report?
 IEEE Trans Software Engineering  V36n5(Sep/Oct 2010)pp618-643 
 =POLL 872 DEVELOPERS 310 REPORTERS BUGS FOSS APACHE ECLIPSE MOZILLA =DEMO TOOL CUEZILLA WEB 
 What developers need != What users provide. 
 CUEZILLA encourages better bug reports from users. 
.Close

ZimmermannWeibgerberDiehlZeller05 
.Open ZimmermannWeibgerberDiehlZeller05 
 Thomas Zimmermann & Peter Weibgerber & Stephan Diehl & Andreas Zeller
 Mining Version Histories to Guide Software Changes
 IEEE Trans Software Engineering  V31n6(Jun 2005)pp429-526 
 =EMPIRICAL EVOLUTION OPEN SOURCE TOOL ROSE CVS ECLIPSE GCC GIMP JBOSS JEDIT KO
FFICE POSTGRES PYTHON
 ROSE::Eclipse_plugin=http://www.st.cs.uni-sb.de/softevo/
 By analyzing data
collected from version histories can predict what else is likely to be 
changed if one location is changed. Top 3 predictions cover correct
predictions 79% of the time.
 Detects undocumented couplings.
 May help prevent incomplete/inconsistent changes.  Few false alarms.
 Fine grain prediction works best on stable systems.  But even unstable systems the files can be predicted,
 Works best in maintenance.
.Close

Zipf47
.Open Zipf47
 G K Zipf
 The Hypothesis of the "Minimum equation" as a Unifying Social Principle: with Attempted Synthesis
 Am Sociol Rev V12(1947)pp627-650
 =STATISTICS MATHEMATICS RANKING CLASSIC
 Power laws:  Rank^power * Size = Constant.
 For example USA metropolitan area populations, n=1 fits well
.Close

ZitserLippmannLeek04
.Open ZitserLippmannLeek04
 Misha Zitser & Richard Lippmann & Tim Leek 
 Testing static analysis tools using exploitable buffer overflows from open source code
 Proc SIGSOFT'04/FSE-12& ACM SIGSOFT Software Engineering Notes V29n6(Nov 2004)pp97-106
 =EXPERIMENT open source SECURITY  TOOLS Boon Archer Uno Splint PolySpace C sendmail BIND WU-FTPD
 Static analysis tools miss known buffer overflows and misdiagnose safe programs.
 PolySpace best.
 Main problem: content of arrays makes code safe/unsafe..
.Close

Ziv00
.Open Ziv00
 Edward A Ziv
 avoiding the iceberg
 Software Development Magazine V8n9(Sep 2000)pp80+78-79
 =EXPERIENCE RISKS MANAGEMENT
 no interest, no plan, no purpose, too much management, too much interuption.
 SMART:= (Specific, measurable, achhievable, related to prime purpose, time.bounded).
 "go for the modest win, and use the second release for new featurs"
.Close

Zobel04
.Open Zobel04
 Justin Zobel 
 Writing for Computer Science 
 Springer-Verlag New York, LLC Edn  2 May 2004 ISBN: 1852338024 Paperback, 270pp 
 =MANUAL WRITING COMPUTER SCIENCE
.Close

Zokaites02
.Open Zokaites02
 David Michael Zokaites
 writing Understandable Code
 Software Development Magazine V10n1(Jan 2002)pp48-50
 =EXPERIENCE TECHNICAL CODING STYLE
 See Kernighan and Plauger 197?
.Close

ZouZhangZhao07
.Open ZouZhangZhao07
 Ying Zou & Qi Zhang & Xulin Zhao 
 Improving the usability of e-Commerce Applications Using Business Processes
 IEEE Trans Software Engineering  V33n12(Dec 2007)pp837-855
 =EXPERIMENT USER INTERFACE BUSINESS WORKFLOW MODEL XML Java 
  Tools derive user interface directly from an encoded model of the workflow and the needed data, forms, and functions.
 Result improves usability for non-expert users.
 Screens show Navigation + Processes + Tasks + Workspace panes/frames.
 The workspace shows only the relevant screens for current Tasks.
.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

ZurMuehlen04
.Open ZurMuehlen04
 Michael Zur Muehlen 
 Organizational Management in workflow application -- issues an perspectives 
 Information Technology and Management V5n3-4(July= 2004)pp271-291 $CR 0605-0529
  =UNREAD =MODEL WORKFLOW CONCEPTS ACTIVITY TRIGGERING vs BPEL 
.Hole 
.Close

Zvegintzov98
.Open Zvegintzov98
 Nicholas Zvegintzov
 Frequently Begged Questions and How To Answer them
 IEEE Software Magazine V15n2(Mar/Apr 1998)pp93-96
 =SCIENCE EMPIRICAL EVIDENCE GRADES
 how to evaluate recorded "wisdom" on empirical questions
 Grades: A:systematically gathered real data; B:poll; C:Isolated data points; D: Isolated data points inside advocacy; E:unattributed assertion; F:Folklore
 Nine Questions:important? Reliable answers? how to get reliable data?
 Answers average D-
 Question 10: Does it matter?
.Close

Zwebenetal95
.Open Zwebenetal95
 Stuart H Zweben & Stephen H Edwards & Bruce W Weide & Joseph E Holingsworth
 The Effects of Layering and Encapsulation on Software Development Cost and Quality
 IEEE Trans on Software Eng VSE-21n3(Mar 1995)pp200-208 CR9601-0271
 =EXPERIMENTS TECHNICAL QUALITY COST
 indicates that using specification info rather than implementation saves time with no loss of quality.
.Close

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

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