Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Poll: Management of Change on annotated code (e.g. jessie)

  • Subject: [Frama-c-discuss] Poll: Management of Change on annotated code (e.g. jessie)
  • From: hbl at sysgo.com (Holger Blasum)
  • Date: Thu, 29 Apr 2010 13:11:21 +0200
Dear "jessie segment of the code annotation community",
 
management of change (e.g. 
 http://en.wikipedia.org/wiki/Change_management_(engineering) ) deals
with processes that have to be executed when issues or new requirements
with source code come up (e.g. in issue tracking tools, version control
systems etc). It is part of quality assurance and well-established in 
a number of standards such as e.g. DO-178B or Common Criteria. 
 
The Frama-C plug-in jessie reasons about source code. 
What I ask is whether anyone is aware of guidelines on/processes
for/papers on management of change where code annotations such as jessie or
more generally other formal methods (say, Isabelle, PVS ...) are used
for proving properties for source code. In this case, management of 
change in this context would include updating properties and/or 
proofs once the underlying source code changes.
 
To be frank, the reason I am asking here is that a reviewer contested
my statement that no well-established guidelines/processes exist (nor
that much research had been done in that field). I've also asked this 
at http://vcc.codeplex.com/Thread/View.aspx?ThreadId=210850 . Of course
it's not nit-picking but I really want to double-check.
 
To sum up: I'm asking for pointers to 
1) research/experimental work about change management of "annotated code" 
2) or even "production-level" integration of "annotated code" into QA 
management of change (e.g. guidelines/standards)
 
Thanks, 

-- 
Holger Blasum (SYSGO AG)