--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on April 2010 ---
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)