Group:
grammar
Group:
natural language
Group:
program proving
Group:
requirement specification
Group:
types of programming languages
Topic:
abstraction as part of language
Topic:
abstraction in programming
Topic:
automated tests of specifications and designs
Topic:
CADES structural modeling with holons
Topic:
calculus of communicating processes
Topic:
communicating sequential processes
Topic:
curried functions
Topic:
design documentation
Topic:
design languages
Topic:
functional programming
Topic:
lambda calculus
Topic:
limitations of formalism
Topic:
logic programming
Topic:
machine independent programming
Topic:
model checker
Topic:
models of parallel computation
Topic:
Petri net
Topic:
problems with logic programming
Topic:
program proof via assertions
Topic:
program proving is infeasible
Topic:
programming as mathematics
Topic:
programming language design
Topic:
proving concurrent programs
Topic:
reduction languages
Topic:
referential transparency
Topic:
safety critical systems
Topic:
semantics by an abstract machine
Topic:
set-oriented languages
Topic:
specification and design of distributed systems
Topic:
specification is infeasible
Topic:
state machine
Topic:
Turing machine
Topic:
type algebras, typed lambda calculus, and type-complete languages
Topic:
van Wijngaarden grammar
| |
Summary
A formal method is using mathematics and logic to describe or analyze a system or program. If a system is logically sound, large classes of errors can not occur.
While attractive, formal methods come with a high cost. They need specialized talent and substantial time. A change may require a reanalysis of the system, making change impractical even when desired. Formal methods will not identify mistaken goals, requirements, and designs.
Formal methods are practical for error-prone domains such as state machines and concurrency. If a program clearly identifies concurrent and state-controlled processes, automated analysis can check for problems.
Formal methods help define the semantics of a programming language. Without a formal semantics, further formal analysis is unfounded.
Formal descriptions can quickly become unwieldly. Tabular presentations help identify components with simple descriptions. (cbb 6/06)
Subtopic: reliability through formalism 
| Quote: more reliable elevator scheduler from formal methods than informal analysis; style also better; study using 20 teams [»sobeAE3_2002]
| | Quote: readable, precise documentation is required; e.g., as input to tools [»hoffDM_2001]
| | Quote: validated BOS's communication protocol with PROMELA and SPIN; identified an unsafe situation where only one door closed; intuitive chart of message sequence [»tretJ9_2001]
|
Subtopic: formal method projects
| Quote: Lucent uses virtual finite-state machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]
| | Quote: the VFSM validator exhaustively exercises a network of communicating VFSMs using the supertrace algorithm; found errors in three tested applications; widely used formal method [»florAR1_1997]
| | Quote: ten commandments for successful projects using formal methods [»boweJP4_1995]
| | Quote: use a small vocabulary for formal methods; easier to understand though longer, more abstract, little implementation bias; e.g., Hoare's CSP [»boweJP4_1995]
| | Quote: use a formal methods team with a traditional design team; catches specification errors early [»boweJP4_1995]
| | Quote: need a formal methods guru when using formal methods in a project [»boweJP4_1995]
| | Quote: the length of a Z specification corresponds to the testing and development effort; useful for scheduling [»tretJ9_2001]
|
Subtopic: requirements
| Quote: use formal methods to verify a design instead of proving correctness; forces engineers to be precise about details; resolves differences of interpretation between implementers and testers [»tretJ9_2001]
| | Quote: formal methods should improve reuse; they clearly state requirements with high component integrity without implementation bias [»boweJP4_1995]
|
Subtopic: formal semantics
| Quote: formal semantics for programming languages should play a fundamental role in software engineering [»parnDL10_1976]
| | Quote: Esterel's formal semantics is based on constructive causality [»benvA1_2003]
| | Quote: formal semantics enables compile-time optimization, analysis, and verification
| | Quote: algorithm for evaluating an applicative expression relative to an environment; first formalization of expression evaluation
| | Quote: operational semantics are good formal methods; intuitive, help implementers, simple, easy prototyping, easy integration [»degaP6_2001]
| | Quote: a meta-circular interpreter for expression evaluation defines each feature of the defined language via the corresponding feature of the defining language [»reynJC8_1972]
| | Quote: formalization of XML Schema using tree grammars; named types and structural types; matching and validation [»simeJ1_2003]
| | Quote: formalization of XML Schema used for XQuery and XPath specifications; one of the first
| | Quote: XQuery standardization unanimously accepted pure named typing due to its simplification of formal semantics [»simeJ1_2003]
| | QuoteRef: tennRD8_1976 ;;443 goes into Scott's formulations of semantic functions
|
Subtopic: mixed formal and natural
| Quote: BOS used formal Z specifications and natural language for detailed design; checked consistency, types, completeness; verified postconditions and invariants for highly critical subsystems [»tretJ9_2001]
| | Quote: formal methods do not help with conceptual models and high-level structuring; both require experience; formal specification gives a false feeling of confidence [»tretJ9_2001]
|
Subtopic: state machine, automaton
| Quote: an automaton is a black box that answers "yes" or "no" to arbitrary, finite sequences of symbols from a fixed, finite alphabet [»rabiMO4_1959]
| | Quote: an automaton's operation is determined by finite, internal states; i.e., stable states of the machine at discrete time intervals; nothing else matters [»rabiMO4_1959]
| | Quote: one-tape, finite automaton are closed under backward tapes and complex products; forms a Boolean algebra of sets [»rabiMO4_1959]
| | Quote: nondeterministic automaton equivalent to finite automaton; many choices at each move, with at least one winning combination; simpler description with fewer internal states [»rabiMO4_1959]
| | Quote: finite automata do not support hierarchical design or concurrency; large, real-time systems are impossible to understand [»benvA9_1991]
| | Quote: Lucent uses virtual finite-state machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]
|
Subtopic: testing
| Quote: formal design specification allows test construction concurrently with coding; ready to test when coding finished [»tretJ9_2001]
| | Quote: testers are effective reviewers of formal design specifications; they use the specifications to write their tests
|
Subtopic: security language
| Quote: secure DNS resolver in 10 lines of code; easier to understand than BIND's security policy [»jimT5_2000]
|
Subtopic: combinators
| Quote: use combinators to find the value of a financial contract; compositional, abstract valuation semantics [»joneSP9_2000]
| | Quote: a financial contract has an acquisition date and an horizon or expiry date; (truncate t c) trims t's horizon to c [»joneSP9_2000]
| | Quote: contracts in terms of observables; i.e., time-varying, objective measurements; e.g., temperature in LA [»joneSP9_2000]
| | Quote: choose to acquire a financial contract (anytime u) or choose either contract (or) [»joneSP9_2000]
| | Quote: use scoped combinators in Haskell for block and unblocking asynchronous interrupts; formal semantics
| | Quote: the expression +/ in J is a tacit definition of summation; arguments are implicit; tacit definition is widely usable [»huiRKW8_1991]
| | Quote: the tacit function 'f g h' is a fork that applies g to the results of f and h; e.g, 'a (+ * -) b' is '(a+b)*(a-b)' [»huiRKW8_1991]
| | Quote: J's primitives are one or two letters, e.g., $y for shape of y, #y for count of y, x,:y append itemized x to itemized y, f^:n y apply f n times to y [»huiRKW8_1991]
| | Quote: APL has two function modifiers (reduction and cross product), but they can only combine with primitives [»backJ_1972]
|
Subtopic: decision table
| Quote: use tables to specify the post-value of a variable for various combinations of pre-values [»parnDL12_1994]
|
Subtopic: asynchronous
| Quote: can interrupt a purely-functional computation at any point; allows asynchronous exceptions [»marlS6_2001]
|
Subtopic: examples
| Quote: used formal methods for BOS, the automated control system for Rotterdam's movable dam; highest safety integrity level; completed on time and within budget [»tretJ9_2001]
| | Quote: validated BOS's communication protocol with PROMELA and SPIN; identified an unsafe situation where only one door closed; intuitive chart of message sequence [»tretJ9_2001]
| | Quote: formal methods were used successfully; all of the software engineers found them useful [»tretJ9_2001]
| | Quote: should have formalized the functional specification as well as the technical design; found problems, errors, ambiguities, and inconsistencies [»tretJ9_2001]
|
Subtopic: history
| Quote: to produce an utterance one has to refer back to general rules and forward to specific rules while reconstructing the rules from continuity, context, and exceptions [»misrVN_1966]
|
Subtopic: problems with formal development
| Quote: formal methods are less understandable than actual program text
| | Quote: dealing with changed requirements is particularly painful for formal program development [»berrDM10_2002]
| | Quote: requirements and proofs are inherently global; a changed requirement may require redoing most of the proofs; verification gets dropped [»berrDM10_2002]
| Quote: a simple error in Z can lead to a correct specification with a completely different meanings; e.g., forgetting a prime symbol ' to indicate the new state
[»tretJ9_2001]
|
Related Topics
Group: grammar (8 topics, 181 quotes)
Group: natural language (16 topics, 539 quotes)
Group: program proving (10 topics, 311 quotes)
Group: requirement specification (11 topics, 307 quotes)
Group: types of programming languages (29 topics, 611 quotes)
Topic: abstraction as part of language (18 items)
Topic: abstraction in programming (67 items)
Topic: automated tests of specifications and designs (12 items)
Topic: CADES structural modeling with holons (24 items)
Topic: calculus of communicating processes (13 items)
Topic: communicating sequential processes (33 items)
Topic: curried functions (14 items)
Topic: design documentation (43 items)
Topic: design languages (12 items)
Topic: functional programming (45 items)
Topic: lambda calculus (16 items)
Topic: limitations of formalism (93 items)
Topic: logic programming (34 items)
Topic: machine independent programming (13 items)
Topic: model checker (49 items)
Topic: models of parallel computation (33 items)
Topic: Petri net (44 items)
Topic: problems with logic programming (10 items)
Topic: program proof via assertions (61 items)
Topic: program proving is infeasible (47 items)
Topic: programming as mathematics (27 items)
Topic: programming language design (53 items)
Topic: proving concurrent programs (37 items)
Topic: reduction languages (17 items)
Topic: referential transparency (26 items)
Topic: safety critical systems (32 items)
Topic: semantics by an abstract machine (38 items)
Topic: set-oriented languages (20 items)
Topic: specification and design of distributed systems (14 items)
Topic: specification is infeasible (46 items)
Topic: state machine (67 items)
Topic: Turing machine (30 items)
Topic: type algebras, typed lambda calculus, and type-complete languages (28 items)
Topic: van Wijngaarden grammar
(9 items)
|
