PROGRAMMING
METHODOLOGY
CONNIE HEITMEYER
Center for High Assurance Computer Systems
Naval Research Laboratory
Washington, DC
Workshop on the Verification Grand Challenge
SRI International
February 21-23, 2005
OUTLINE
•
•
•
•
Background: The SCR toolset
Programming Methodology
– State of the art
– State of the practice
Mathematics vs. Engineering
– Components of a well-founded software engineering
discipline
How to deal with legacy code
– An alternative proposal
2/24/05
2
SCR TOOLSET: HISTORY AND OVERVIEW
•
I am the chief designer of the SCR toolset, which supports the
specification of requirements in the SCR tabular notation
–
•
•
•
•
•
2/24/05
Based on original A-7 requirements method originated by Dave Parnas et al.
in the late 1970s
Major objective of the SCR method and tools 
To produce a validated, verified requirements specification
Attributes of a high quality requirements spec
–
–
–
–
Precise and unambiguous
Readable by practitioners AND customers
Complete and consistent; correctness validated by domain experts
Freedom from implementation bias
Benefits of a high quality requirements spec - solid basis for
–
–
–
Automated test case generation (satisfying some coverage criterion)
Automated generation of provably correct, efficient code
Developing a new version of the system
Other major benefit - serves as a precise means of communication between
all of the stakeholders: the customers, the future users, the developers, etc.
SCR tools have been used in over 30 university courses, conference tutorials,
and industry tutorials
3
SCR TOOLS
SCR
TOOLSET
•
•
•
most mature tools
Distributed to
200+ org’ns in
industry, govt.,
and academia
Focus on safetycritical, securitycritical systems
ANALYSIS
TOOLS
• TAME is an
interface to PVS
designed to prove
properties of state
machine models
system
spec
SPECIFICATION
EDITOR
DEPENDENCY
GRAPH BROWSER
modes
terms
CONSISTENCY
CHECKER
conditions
cont vars
events
SIMULATOR
mon vars
MODEL
CHECKER
THEOREM PROVER
(TAME)
PROPERTY
CHECKER (Salsa)
INVARIANT
GENERATOR
TEST CASE
GENERATOR
CODE
GENERATOR
Research Prototypes
Current focus: Optimized, provably
correct code
APPLICATIONS TO
PRACTICAL SYSTEMS
Since 1999, at least three sites of Lockheed Martin have been using the SCR
tools to develop critical avionics software
•
•
•
•
Largely embedded software -- tends to have highly complex control logic, functions
with many parts, simple data types
Representative applications: flight navigation, flight guidance, autopilot logic, flight
management, traffic and collision avoidance, and security testing
Tools also being applied to software for the Joint Strike Fighter
LM uses specs developed with tools to automatically generate a suite of test cases
Comment
from a
(mostly)
satisfied
We currently are supporting close to 1500 models … and have found the
user
SCRTool suite to be an invaluable aid in finding requirements defects, as
well as validating the functional behaviour of our software requirements.
S. D. Allen, Lockheed Martin
January 10, 2005
2/24/05
5
PROGRAMMING METHODOLOGY:
STATE OF THE ART
•
Many useful principles and guidelines have been formulated for
application in software development
•
•
•
•
•
•
Design for ease of change
Stepwise refinement
Separation of concerns
Specifications that are simultaneously easy to understand, precise and
unambiguous and that avoid implementation bias
• Requirements that describe the needed software behavior as a relation on
environmental quantities…
Lots of specification and modeling languages, methods, methodologies,
and tools have been proposed by researchers
• Languages: Z, B language, CSP, CCS, SCR, RSML, Aslan, Statecharts, Esterel,
Lustre, Signal, TRIO, I/O automata,…
• Methodologies: Object-Oriented (UML, Eiffel, Alloy, …); Aspect- Oriented;
Extreme Programming; Agile Programming; ASMs; Model-Driven Design
Problem: No consensus among software engineering and other
researchers on which specification/modeling languages, methods, and
methodologies practitioners should use to develop reliable software
– No agreement on what constitutes a good model
– Few good examples of high quality specifications
2/24/05
6
PROGRAMMING METHODOLOGY:
STATE OF THE PRACTICE
•
•
•
The overwhelming majority of existing software, even software for
safety-critical, security-critical systems, has been built and is being
built in an ad hoc, unsystematic fashion
The vast majority of software developers continue to focus on code
– While they may write requirements and design documents, these
documents are almost universally incomplete, inconsistent, incorrect, and
poorly organized.
The vast majority of software developers do not develop specifications
of the required software behavior
– Few specifications, let alone high quality specs, are developed
– Specifications that do exist are often low-level and filled with design and
implementation bias
•
Very few software developers use theorem provers or model checkers
•
Two bright spots
2/24/05
– Many are undereducated -- they cannot do formal proofs nor do they even
understand propositional logic let along 1st order logic
– For the ones who could potentially do formal proofs or apply a model
checker, the view is that verification tools are NOT cost-effective and
there is little evidence to prove them wrong
– Increasing use of Java
– Growing popularity of model-driven design
7
MATHEMATICS VS.
ENGINEERING
MATHEMATICAL
RESOURCES
(e.g., theories, models,
and algorithms)
Theories for deductive verification,
Theory underlying model checking,
SAT solvers, BDDs, etc.
Automata theory and models
Theories underlying decision
procedures and their combination
Tools based on fundamental research
…
MATHEMATICALLY
WELL-FOUNDED
SOFTWARE
ENGINEERING
DISCIPLINE
Methods
Models
Languages/Templates
Industrial-Strength Tools
LONG-TERM GOAL
Semi-Automatic Transformation of a Specification
into a Provably Correct, Efficient Program
Claim: Developing a well-founded software engineering discipline is of
comparable importance to scientific advances
2/24/05
8
A WELL-FOUNDED SOFTWARE
ENG. DISCIPLINE: COMPONENTS
•
•
•
•
•
•
•
•
•
2/24/05
Specification languages customized for particular domains (e.g.,
control systems, office systems, web programs, protocols, …)
Powerful, robust, integrated tools that are easy to use
– Model checkers coupled with simulators
– Simulators with nice graphical interfaces
Templates for specifying system-level (and other) properties
Proof systems that produce understandable proofs, e.g., a step
in the mechanized proof corresponds to a step in a hand proof
– Example: TAME interface to PVS uses PVS strategies to raise level
of theorem proving to level of human reasoning
– From a TAME proof, a human-understandable proof can be
constructed [Archer+, ASE, 2002].
Compilers that generate provably correct, efficient code from
high-level specifications
Automatic generation of invariants satisfying some specified
coverage criterion
Specification-based automatic test case generation
Good examples of high quality specs and models
Libraries of programs and program modules (including specs,
properties satisfied, and proofs of correctness)
9
HOW TO DEAL WITH LEGACY CODE:
AN ALTERNATE SOLUTION
EXTRACT A SPEC FROM THE CODE
BENEFITS OF A SYSTEM-LEVEL SPEC
1. Flexibility in code generation
– Can choose from many desired target languages
– Possibly, more efficient code
2. Easier to understand/reason about the software
– Higher level of abstraction
3. Improve potential for interoperability
– Easier to know how to use the software as part of a
larger system
4. Easier to modify and maintain the software
5. Easier to assess the software
– e.g., generate good test suites
6. The process of developing the spec will expose bugs
(although how to eliminate them may be tricky)
2/24/05
10
EXTRACTING A SPEC FROM THE CODE:
TECHNICAL APPROACH
domain experts,
system users,
system/user documentation
legacy code
code annotations
1. Generate elements needed
to build operational spec
system modes, transitions, ...
scenarios, system invariant props.
inputs/outputs,
program units, …
Iterate until
spec and
legacy code
conform NO
conforms?
conforms?
YES
2. Synthesize
operational spec
test cases, operational spec
legacy code
3. Test conformance of
operational spec with
legacy code
operational spec
4. Construct
replacement code
2/24/05
11
Descargar

No Slide Title