categories and formal verification

[David CHEMOUIL <David.Chemouil@onera.fr>]

Dear colleagues,


Some colleagues of mine and myself are currently investigating categorical
approaches to component-based development for software, in the spirit of J.
L. Fiadeiro's work or of the coalgebra community.

Being new to the discipline, it also implies for them quite some work in
basic CT itself. Hence, they're looking for some kind of reason making this
tedious process worth enduring. Elegance of CT is one such reason, Goguen's
or Ehrig's arguments in a few articles are others.

But, although my colleagues, are pretty convinced by the "constructive"
aspects of CT applied to such matters, they don't see how CT can provide
support in *verifying* things about systems under study (e.g what does CT
approaches bring to check the absence of deadlocks in a concurrent system?).

I couldn't find convincing examples, even in Goguen's Manifesto, so I
wondered whether you had good arguments and/or references to such convincing
work, that would give them the impetus to continue studying this topic.

Regards,

dc
-- 
David CHEMOUIL
ONERA/DTIM
http://www.onera.fr/staff/david-chemouil


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]