[Bug 486757] New: Review Request: divine-mc - Multi-core model checking system for proving specifications
bugzilla at redhat.com
bugzilla at redhat.com
Sat Feb 21 20:36:15 UTC 2009
Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.
Summary: Review Request: divine-mc - Multi-core model checking system for proving specifications
Summary: Review Request: divine-mc - Multi-core model checking
system for proving specifications
Component: Package Review
AssignedTo: nobody at fedoraproject.org
ReportedBy: dwheeler at dwheeler.com
QAContact: extras-qa at fedoraproject.org
CC: notting at redhat.com, fedora-package-review at redhat.com
Estimated Hours: 0.0
Spec URL: http://www.dwheeler.com/divine-mc.spec
SRPM URL: http://www.dwheeler.com/divine-mc-1.3-1.fc10.src.rpm
DiVinE Multi-Core (MC) is a parallel shared-memory enumerative model-checking
tool for verification of concurrent systems. The tool can employ the full
power of modern 64-bit multi-core architectures.
It can be used to prove correctness of verification models as
well as to detect early design errors.
Any model-checking tool, such as DiViNe MC, accepts system requirements or
design (called models) and a property (called specification) that the final
system is expected to satisfy. The tool then outputs yes if the given
model satisfies given specifications, and generates a counterexample
otherwise. The counterexample details why the model doesn't satisfy
DiViNe MC is based on automata-theoretic approach to
linear temporal logics (LTL) model checking.
The input language allows for specification of processes in terms of
extended finite automata and the verified system is then obtained as
an asynchronous parallel composition of these processes.
In the current DiVinE Multi-Core release, input is provided in DVE format --
an industry-strength specification language, as used in original
DiVinE, with plenty of diverse example models, ranging from simple toys
to complex real-world models. An extensive model database is available
at BEEM database.
Moreover, DiVinE can read models specified in ProMeLa (as used in the SPIN
tool), in addition to its native DVE format. However, the capabilities of
the tool on ProMeLa models is currently limited by inability to produce
counterexamples: you can only obtain a yes/no answer.
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.
More information about the package-review