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

Bibliography Retrieval Engine(Beta)

Items in bibliography identified by a string matching Lamport

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.


(Search uses POSIX regular expressions and ignores case)

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