Task VC[2]: Verification Support for Heterogeneous Processes

To develop verification support for heterogeneous processes, we investigate techniques to decompose complex propositions into a combination of propositions in individual logics. Based on experience with HOL-CSP, CSP-PROVER and CSP-CASL, we develop hetero- geneous proof calculi that combine available proof calculi for the process description with available proof calculi for the logic used for data representation, and moreover provide support for new heterogeneous constructs including the heterogeneous abstraction views developed in Work Package RA. The key aspects here are to identify powerful tools which can handle propositions in specific logic fragments (e.g. model checkers such as FDR, Spin, Uppaal, SMT provers, or SAT checkers), and develop a methodology how to decompose propositions and compose results from these tools in a more general framework, building on previous work on combining model checking and theorem proving by techniques such as data independence.

All Tickets

Ticket Priority Summary Owner
No tickets found

Last modified 8 years ago Last modified on 25.02.2011 10:44:17