lkml.org 
[lkml]   [2003]   [May]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: inventing the wheel?
Carl-Daniel Hailfinger wrote:
> Now we only need one additional tool to *prove* correctness of the
> kernel ;-)

Perhaps another interesting approach for such source code analyzers
would be to take a top-down view, i.e. assume a certain functional
structure, and check that all the elements are there and in the
right order.

This should be feasible for code that basically follows a certain
template, e.g. network card drivers.

This would also help with the update problem of "fill in the blanks"
type of templates, i.e. if the template changes or is augmented,
some drivers using it may no longer conform to it.

Such a top-down view could be layered on top of a bottom-up analyzer,
e.g. by - manually or automatically - translating some "skeleton"
into a set of rules of the type "if you've called X, you must later
call Y", etc.

- Werner

--
_________________________________________________________________________
/ Werner Almesberger, Buenos Aires, Argentina wa@almesberger.net /
/_http://www.almesberger.net/____________________________________________/
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at http://vger.kernel.org/majordomo-info.html
Please read the FAQ at http://www.tux.org/lkml/

\
 
 \ /
  Last update: 2005-03-22 13:35    [W:0.079 / U:1.612 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site