Loading presentation...
Prezi is an interactive zooming presentation

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

(DANSAS) Tool-supported Refinement-centric Analysis, Design, Development and Verification

A big-picture view of our work on rigorous, refinement-centric software engineering from analysis to verification in using EBON, JML, and Java.
by

Joseph Kiniry

on 20 August 2010

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of (DANSAS) Tool-supported Refinement-centric Analysis, Design, Development and Verification

Tool-supported Refinement-centric Analysis, Design, Development and Verification Joe Kiniry
IT University of Copenhagen

DANSAS
19 August 2010 The EBON language must:
1. ...have a (mechanically specified) semantics.
2. ...have both a graphical and a textual notation.
3. ...describe both static and dynamic aspects of an architecture.
4. ...be language neutral and programming style neutral.
5. ...be extensible by non-programmers with new semantically meaningful constructs.
6. ...have a formal refinement to popular specification and programming languages.
7. ...support writing high-level specifications like features and requirements in English.
8. ...support formal model-based specification using assertions.
9. ...have a formally defined refinement.
10. ...support static reasoning about and within a model and the language's metamodel.
11. ...support both refinement checking and refinement generation.
12. ...support traceability between engineering artifacts.
13. ...have quality tool support in the manner which modern programmers expect. Fintan Fairmichael Eoin O'Connor Ralph Skinner Eva Darulova Dragan Stosic Aidan Morrissey EBON
The Extended/Extensible Business Object Notation class_chart CAGE
explanation
"An enclosure that holds animals in a zoo."
inherit
ENCLOSURE
command
"Make this cage larger to this square meterage.",
"Paint this page this color."
query
"How tall is this cage?",
"How wide is this cage?",
"How many cats does this cage contain?",
"How many occupants does this cage contain?",
"What is the maximum capacity of this cage?"
constraint
"The number of cats must always exceed the number of mice.",
"The number of bugs must be below 100.",
"The number of mice must be at least 50.",
"The number of snakes must be no more than 10."
end EBON
The Extensible/Extended
Business Object Notation Goals Develop a high-level specification language that seamlessly covers system analysis and design.
Build a modeling tool that formal methods researchers will appreciate.
Keep architecture descriptions always up-to-date using novel forms of refinement.
Generate architecture descriptions from implemented systems, and generate system templates from architecture descriptions.
Statically check that refinements between different specification levels and artifacts are preserved. The end-users of this work are meant to be both "normal" software engineers who wish to document their requirements, features, and architectures
and
formal methods researchers interested in model-driven and rigorous approaches to software engineering . Any questions?
Full transcript