Verification process modelling and improvement

Verification process modelling and improvement is one activity of the Trustworthy Systems project inside the Software System Research Group (SSRG).

• Aim: efficiently and effectively building large-scale trustworthy systems by

  • making small-scale (up to 30K LoC) full-code formal verification methods repeatable,
  • devising new processes for building and verifying large-scale systems (millions LoC), and
  • understanding architecture-process relationship.

• Latest news:

  • The paper Large-Scale Formal Verification in Practice: A Process Perspective published at ICSE 2012
  • The paper Simulation Modeling of a Large Scale Formal Verification Process published at ICSSP 2012
  • A number of people participated in a joint Workshop at ISCAS in Beijing in May 2012.
  • The paper Impact of process simulation on software practice: an initial report published at ICSE 2011

• Context:

  To combine untrusted components with formally verified or synthesised trusted components at the scale of millions lines of code, we need to empirically understand the cost and development process implications of full-code verification itself and its effects on building larger systems. This will make formal verification processes more repeatable/predictable and create new processes better integrating the formal approach for developing large-scale trustworthy systems.

• Technical research challenges:

  • modelling verification processes with the right-level of details
  • analysing and improving verification processes through mixed discrete and continuous process simulation
  • identifying cost factors, sizing/complexity metrics and experience patterns
  • using system architectures as inputs to process optimisation and improvement
  • using process constraints as inputs to architecture analysis

• Contact: Liming Zhu, liming.zhu<at>nicta.com.au

People