|| [News] || [Research]

AbadiLamport90 .Open AbadiLamport90 Martin Abadi & Leslie Lamport Composing Specifications Digital Sys Res Center(Oct 10 1990) CR9405-0309 F.3.1 .See [AbadiLamport93] =MATHEMATICAL SPECIFICATION LOGIC Has a ref to Cliff Jones's Oxford PhD Thesis in the early 80s! p9: "Composition is conjunction" cf Zave & Jackson. .Close AbadiLamport92 .Open AbadiLamport92 Martin Abadi & Leslie Lamport An Old-fashioned Recipe for Real Time Digital Sys Res Center TR#91(Oct 12 1992) .See [AbadiLamport94] =MATHEMATICAL TIMING LOGIC .Close AbadiLamport93 .Open AbadiLamport93 Martin Abadi & Leslie Lamport Composing Specifications ACM TOPLAS V15n1(Jan 1993)pp73-132 =MATHEMATICAL SPECIFICATION LOGIC Reviewed CR9405-0309 F.3.1 similar to AbadiLamport90 Based on Lamport91 .Close AbadiLamport94 .Open AbadiLamport94 Martin Abadi & Leslie Lamport An Old-fashioned recipe for Real Time ACM TOPLAS V16n5(Sep 1994)pp1543-1571 See .See [AbadiLamport92] =MATHEMATICAL TIMING LOGIC Review CR9507-0506 F.3.1: uses TLA as a base can reason separately about function and timing(by var now:real). Two problems: now can get stuck (Zeno-ness) or two requirements can conflict. ->> detect and correct spec to avoid. (not in A&L 1992?) .Close AbadiLamport95 .Open AbadiLamport95 Martin Abadi & Leslie Lamport Conjoining Specifications ACM Ttrans Prog Lang Sys V17n3(May 1995)pp507-535 CR9605-0369 CR9608-0610(...cumbersome notation....) F.3.1 =MATHEMATICAL SPECIFICATION LOGIC TLA conjunction implies parallel combination .Close Champeaux02 .Open Champeaux02 Dennis de Champeaux Software Engineering Considered Harmful Commun ACM V45n11(Nov 2002)pp102-104 =ESSAY ENGINEERING SCIENCE LOGIC PRACTICE C++UML VALIDATION Quotes Denning on the state of current software systems and being hired to fix messes that should not have occurred. Need for extensions to Hoare Logic to pointers and parallel processes. Seems to ignore work by Hoare, Lamport and others. .Close ErnstHookwayOgden94 .Open ErnstHookwayOgden94 George W Ernst & Raymond J Hookway & William F Ogden Modular Verification of Data Abstractions with Shared Realizations IEEE Trans SE-30n4(Apr 1994)pp288-307 .Box Note ADTs export types modula RESOLVE From Abstract: "The abscence of side-effects must be explicitly proven by the verification method. This requires the specification language to provide for quantification over the currently active (allocated) instances of an abstract type" Abstraction is a mixture of code and specification invariant, require, and ensure assertions Automatic initializations IntegerSet example Quantification `for Q x:1..alloc( ... R[x] ....)` Variable x (an object of exported type) is replaced by R[x] inside. Assume and Confirm statements MetaTheory ??Lamport/Lam Shankar?? ->p304: "A valid program is a collection of valid modules in which each item imported by a module is exported by precisely one other module, and in which the specs of imported and exported items are compatible" .Close.Box .Close KayReed93 .Open KayReed93 Andrew Kay & Joy N Reed A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange IEEE Trans SE-V19n6(Jun 1993)pp625-639 =THEORY MODULES NONSEQUENTIAL SAFETY LIVENESS PROOF PERFORMANCE .Box p631: "The correctness proofs for the design require that the time for internal signal be very small compared to times between externally generated signals." need expertise to recognise and handle race conditions p629: Rely/garantee works without extra conditions as long as: (1)No safety constraints on inputs and (2) every component polls its all its inputs p638: "Our main objective was to prove that desirable things happen within a given time" p635: "...proofs often revealed faults in our proposed design" Uses DFD-like diagrams p630:"The first version of the specification, as is inevitable in any non-trivial application, did undergo a certain amount of change during the design phase" p625: "Masses of useless formal scribblings" avoided by "CSP specification style of giving predicates over sets of traces of the system (and its components) can result in more abstract specifications than those in a state/transition style, and hence are less detailed" "Components do not have behave correctly in every invironment, but if each component satisfies its individual specification the behavior of the composite system is not compromised" ..."The rely and guarantee parts of the specification are collected to form interface specifications, making for a high level of organisation with the minimum of effort". Has ref to Cliff Jones D. Phil thesis Oxon Jun 1981 Should have ref to .See [Lamport90b] perhaps. TCSP::=Timed CSP traces with refusal sets - research/1 notes/kay&reed/... prevents, causes, rely and guarantee P O T S: Spec with 24 rely/guarantee pairs .Close.Box .Close Lamport86a .Open Lamport86a Leslie Lamport Control Predicates are Better than Dummy Variables for Reasoning About Program Control Report 11 Systems Research Center Digital Equipment Corpn May 5th 1986 =THEORY NONSEQUENTIAL FORMAL .Close Lamport86b .Open Lamport86b Leslie Lamport A Simple Approach To Specifying Concurrent Systems Report 15 Systems Research Center Digital Equipment Corpn Dec 25th 1986 =THEORY non-sequential formal specification .Close Lamport87 .Open Lamport87 Leslie Lamport win and sin: Predicate Transformers for Concurrency Report 17 Systems Research Center Digital Equipment Corpn May 1st 1987 =THEORY non-sequential formal .Close Lamport90a .Open Lamport90a Leslie Lamport A Temporal Logic of Actions(TLA) Report 57 from Systems Research Center Digital Equipment Corpn(1st Apr 1990) & Revised as Lamport91 =MATHEMATICAL non-sequential formal dynamic modal logic .Close Lamport91 .Open Lamport91 Leslie Lamport The Temporal Logic of Actions(TLA) Report 79 from Systems Research Center Digital Equipment Corpn(25th Dec 1991) =MATHEMATICAL non-sequential formal dynamic modal logic Revision of Lamport90b .Close Lamport94a .Open Lamport94a Leslie Lamport Processes are in the Eye of the Beholder Report #132 from Systems Research Center Digital Equipment Corpn(25th Dec 1994) =THEORY NONSEQUENTIAL LOGIC .Box (abstract) A two-process algorithm is shown to be equivalent to an N-process one, illustrating the insubstantiality of processes. A completely formal equivalence proof in TLA (the Temporal Logic of Actions) is sketched. .See http://www.research.digital.com/SRC/publications/src-rr.html .Close.Box .Close Lamport94b .Open Lamport94b Leslie Lamport Unknown ACM TOPLAS (May 1994)pp872-923 =MATHEMATICAL non-sequential formal dynamic modal logic Cannonical version of .See [Lamport91] TLA Temporal Logic of Actions. .Close Lamport94c .Open Lamport94c Leslie Lamport Writing Proofs Microsoft Research .See http://research.microsoft.com/en-us/um/people/lamport/proofs/proofs.html =IDEA PROOFS FORMULAS STRUCTURED FORMAL LOGIC MATHEMATICS Published off line as .See [Lamport95] below. .Close Lamport95 .Open Lamport95 Leslie Lamport<lamport@src.dec.com> How to Write a Proof American Math Monthly V102n7(Aug-Sep 1995)pp600-608 =DEMO PROOFS FORMAL LOGIC .Box Hierarchically structured proofs in outline style see Abadi & Lamports work. Q.E.D. is a step representing what needs to be proved: .As_is Theorem <statement> .As_is PROOF SKETCH: <english style proof scetch> .As_is ASSUME: <label>. <predicate> ... .As_is PROVE: <predicate> .As_is NumberedList( <number>. <step|predicate> ) .As_is <number>. Q.E.D. .As_is LET: <definitions> .As_is Choose .... such that.... .As_is CASE: statement of assumption is short for .As_is ASSUME: Statemnt of assumption .As_is PROVE: Q.E.D. .Close.Box Also see online reports .See [Lamport94c] .Close Lamport95a .Open Lamport95a Leslie Lamport TLA in Pictures IEEE Trans SE VSE-21n9(Sep 1995)pp768-775 =THEORY TLA Formal Graphics temporal logic of actions .Box Claims: first use of diagrams to provide complementary multiple formal views. an aid to presenttion and proof. Like FSA(states=>predicates, transactions => actions) out(n):edges out of n, d(e) :nodes=destination of edge e, P(n) :=predicate on node n, P'(n) :=primed predicate... disjoint_predicate:=for all nodes n1,n2(not(P(n1) and P(n2)). A(n) :=for some e:out(n)(action(n) and P'(d(e))) two possible formula for meaning of transitions: \Delta:=for all nodes n, always(if P(n) then A(n) ) or \Delta_bar:=always(some nodes n(P(n) and A(n))). ()|- if \Delta then \Delta_bar ()|- if disjoint_predicates then (\Delta iff \Delta_bar) .Close.Box .Close LamShankar94a .Open LamShankar94a Simon S Lam & A Udaya Shankar A Theory of Interfaces and Modules I -- Composition Theorem IEEE Trans SE V20n1(Jan 1994)pp55-71 =THEORY SAFETY LIVENESS MODULARITY PROOF COMPOSITION See .See [Jonsson94] .See [KayReed93] .See [ChandyMisra88] .See [AbadiLamport93] .Box Need to divide up software into modules that can be designed separately. Then need to know that when the pieces are composed the whole will work. Proposes a formal model of the ways that modules interface. Defines what it means for a module to satisfy an interface(M offers I, and M offers I using L). Assumes this forms a DAG. Shows that such systems can be composed. Interfaces are two sided - providers and consumers of services. Both sides are designed to not perform badly if the other side performs ok. The provider is designed to guarantee that the service is provided some time after it is requested. Providing a service is a conditional progress properties. Object-oriented programming only specifies safety (lack of bad results). .Close.Box .Close Marketal93 .Open Marketal93 William Mark & Sherman Tyler & James McGuire & Jon Schliossberg Commitment-Based Software Development IEEE Trans SE-V18n10(Oct 1992)pp870-885 =DEMO Comet LOOM AI DESIGN TOOL SEMANTIC .Box (1) Binary search is committed to using sorted data :. It requires either sorted data or a module to sort data. (2) Sending a message implies a module that accepts such a message. commitment as a kind of coupling cf Lamport, Meyer, dependency LOOM - Semantic net expressed in LISP fast at detrmining some subsumption p870:" A major problem for software developers is judging how a change in a module affects and is affected by the rest od the design[...] developers spend much of their time responding to changes" Not maintenance but fresh start so Fails to tackle problem of legacy code: p870: "With the current code-plus-comments descriptions of modules, commitments are implicit[...] in the heads of the developers (and later, to a much lesser extent, in design documents)." p883:"any reasonably expressive description representation language will not allow complete, tractable classification reasoning. So we are in the usual bind: the module description langugae must be expressive enough to encode the fine shades of meaning that can differentiate potential substitute modules from inappropriate candidates, but the system must be able to rapidly discover at least most of the candidates most of the time." .Close.Box .Close Shankar93 .Open Shankar93 A Udaya Shankar An Introduction to Assertional Reasoning for Concurrent Systems ACM Computer Surveys V24n3(Sep 1993)pp225-262 =Tutorial concurrency fairness safety non-sequential temporal logic Prereq for LamShankar94 & Jonsson94... refers to Lamport, UNITY, Mana et al .Close

Search for bibliographic items containing a matching string.

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