Geek Answers Handbook

A tool to test the model of large, distributed C ++ projects such as KDE?

Is there a tool that can handle modeling of large, real, mostly C ++, distributed systems such as KDE?

(KDE is a distributed system in the sense that it uses IPC, although usually all processes are on the same machine. Yes, by the way, this is a valid use of a "distributed system" - checking Wikipedia.)

The tool should be able to handle intra-process events and messages between processes.

(Suppose that if the tool supports C ++ but does not support other things used by KDE, such as moc, we can hack something together in a workaround.)

I gladly accept less general (e.g., static analyzers specialized to search for specific error classes) or more general alternatives to static analysis, instead of real control models. But I'm only interested in tools that can really handle KDE size and complexity projects.

+5
source share
3 answers

You are obviously looking for a static analysis tool that can

  • analyze c ++ on a scale
  • find code snippets of interest
  • model extraction
  • pass this model to model check
  • let the result be for you

, , . , , , , , , , , IMHO .

, , , , - ?

, , . Coverity , , , - Java.

, , : C/++ VeriSoft. [PDF] VeriSoft. , . Verifysoft Bell Labs , , .

: ++.

, ++, : C/++.

, , , - ++ ( ) , . ++, ; , ++ . , , ++. (SPIN ) .

DMS Software Reengineering Toolkit ++ Front End, ++. , , . .

DMS C C (19 000 !). ++ ++, . DMS, , , , . YMMV.

+5

, . , .

, "", . , ( "a == b + 1", ) , . , , , , , - . .

+1

The usual way to apply formal methods to large systems is their modularity and writing specifications for the interfaces of each module. Then you can check each module independently (when checking a module, you import the specifications, but not the code, of the other modules that it calls). This approach makes validation scalable.

0
source

More articles:


All Articles