2nd RefineNet Meeting - Problems
13-14 May 2005
Wilson Ifill: Code generation
- Novice user problem
- How to get novice users going in the right direction
when starting to use a tool, even if they don't read the manual.
- Reduce maintenance costs
- Code generation is a
promising way to save costs on maintenance (which may be up to
four times original development cost) - keep code and spec
more closely aligned.
- Library tweaking
- While developing, you end up going back to the libraries
of the translator and tweaking
them for a while. Until they're frozen you don't win.
How to freeze as early as possible?
- Tool assurance
- If tool tweaking not done by user, but by
supplier - do we trust supplier? UK Defence Standard
00-55 vs DO-178B: how do we support those standards?
- Proving the right thing
- UK Defence Standard 00-55 mandates formal techniques and
independent proof checking - but how do you know that
you've proved the right things? Are your proofs adequate
and complete? can you match up VCs to specifications?
Michael Leuschel: Pro-B
- User feedback
- It would be very useful to have feedback from workshop
on refinement using Pro-B.
- Efficient refinement checking
- What are the issues about designing specifications
which are to be refined; what makes them efficient/
inefficient to check?
- What are useful ways to explore specifications?
Look at lazy exploring of refinement.
- B standard
- Arising out of the RODIN project - there is some talking
about a real B standard (as opposed to just the B Book?)
How should this be formulated? Does Z set a good or bad
precedent for this?
Martin Henson: Grand Challenge Workshop (GC6)
- Contexts for refinement
- Think about refinement in the broader context of evolution,
integrating with high-level system architecture. There is
expertise in RefineNet (and associated departments) on this.
- A Grand Vision for refinement
- GC6 only has one big theme, big project
(the verifying compiler) - idea with long pedigree.
Since GC supposed to last 15-20 years with
an outstanding vision - vision seemed to be very limited in most
submissions, very parochial and personal. Can we do better?
- "Crash-proofing the national information infrastructure"
- "Raise developer productivity by a factor of 10"
Adrian Hilton: Refine to Diverse Hardware
- Premature detail in specification
- Get the customer to tell us what to do rather than
how to do it.
- Translate a formalised requirement back into an English
text - is it useful? Reformulation?
Maybe animate it and let the customer go off and play with
this; does it pay back?
- How to establish completeness of requirements given the specification
(NB lots of work done on requirements capture).
- Retrenching a specification
- Retrenchment allows people to make partial, imprecisely fitting
models, then pull it back and forward to a specification.
Can we make this pay off in concrete examples.
- Timing and preemption in real systems
- There are different notions of clocks in different parts of
a typical real-time system (e.g. bus, microprocessor, ASICs).
Abstract "something may come in" and you chose an appropriate
operation to get the required output. But in a refinement,
in one clock cycle you may only be able to do 2/3 of this task,
then a Built-In-Test (BIT) may come in and wreck the invariant.
This comes down to having some information about what the
RTOS or tasking profile provides. E.g., hiding may be appropriate
but we don't know prima facie enough about the system CBIT/IBIT
- RTOS API
- Most embedded systems run on a Real Time Operating System (RTOS)
which provides essential system services. Refining to this target
produces the problem of what the RTOS API looks like in a
formal model. How do we get the vendors to write a spec in a
generally useful way?
- Invariant violation
- If the spec for a system is in terms of outputs vs inputs, and
the system may shutdown, there
may be a violation of the invariant in the shutdown path - we need
to deal with this. The
more general problem is that you often go back and rework the safety
spec after implementation, weakening it as a result of handling errors
in the code where the error handling breaks the spec
- Refinement payoff
- Draw the boundary for where refinement is appropriate in
a system, and where it's not enough of a payback.
David Crocker: Building a Refinement Tool for Software Development
- Data storage in external subsystem
- Example of stock control - want to hold stock info in an external database
rather than an internal variable
Need to refine abstract data to data in an external system -
refinement no longer valid if no other agent interferes with data,
also need to manage errors (e.g. n/w failure)
- Specifying and refining concurrent systems
- Big problem - how to refine a spec to a multithreaded implementation,
how to express it in a programmer-friendly notation?
More difficult because parallel programming facilities in the
various target languages aren't that alike.
C++/Java threading models - C++ probably Posix, but that means
a lot of work in generation from a common Perfect-Developer language
program. Applicable generally to refinement - need to decide what
we want to refine *to*.
- GUIs and user interaction
- How do you specify/refine to a system like this?
Specialist tools are usually required for GUI programming;
on the other hand, you'd like to be able to
specify the behaviour.
- Reusing unspecified libraries
- Similar problem to RTOS API; either you need to develop your
own libraries, or to retro-specify existing ones.
Associated with that, libraries moving under the project's
feet is an issue. Retro-spec is a
a serious problem - probably infeasible automatically.