bppy.analysis package

Submodules

bppy.analysis.bprogram_converter module

class bppy.analysis.bprogram_converter.BProgramConverter(bprogram_generator, event_list, bt_names=None, max_trace_length=1000)

Bases: object

A class to convert a behavioral program to a PRISM model by exploring the DFS graph.

collect_structure()

Generates the tree structure and other necessary details of the behavioral program.

to_prism(output_file=None)

Converts the behavioral program to a PRISM model of a markov decision process, with each bthread corresponding to a module. Returns the resulting text content.

Parameters

output_filestr, optional

Name of the file to write the PRISM model to. Defaults to ‘None’.

bppy.analysis.dfs_bprogram_verifier module

class bppy.analysis.dfs_bprogram_verifier.DFSBProgramVerifier(bprogram_generator, max_trace_length=1000)

Bases: object

A class to verify a behavioral program using Depth First Search (DFS). Currently, this class verifies only properties which can be defined using assertions in b-threads. For additional properties, or programs with large state space, use SymbolicBProgramVerifier.

Attributes:

bprogram_generatorfunction

A function that generates a new instance of the BProgram.

max_trace_lengthint

Maximum length of the trace before terminating the search.

verify()

Execute a DFS on the behavioral program to check for assertion errors.

Returns:

bool:

True if no assertion error is encountered, otherwise False.

Optional[tuple]:

Trace leading up to the assertion error, if one is encountered. Otherwise, None.

bppy.analysis.symbolic_bprogram_verifier module

class bppy.analysis.symbolic_bprogram_verifier.SymbolicBProgramVerifier(bprogram_generator, event_list)

Bases: object

A class to verify a behavioral program symbolically using PyNuSMV. The verifier can operate in two modes: Binary Decision Diagrams (BDD) and SAT-based Bounded Model Checking (BMC).

Note:

1. The class requires the installation of PyNuSMV. More info on its installation can be found at https://github.com/LouvainVerificationLab/pynusmv.

2. The verifier is currently limited to b-programs with SimpleEventSelectionStrategy.

3. The verifier does not support events with data.

Attributes:

bprogram_generatorfunction

A function that generates a new instance of the BProgram.

event_listlist

List of all possible events in the system.

verify(spec, type='BDD', bound=1000, find_counterexample=False, print_info=False)

Verifies a given specification against the behavioral program.

Parameters:

specstr

The specification to be verified, in NuSMV LTL specification format.

typestr, optional

The verification type to be used: Binary Decision Diagrams (“BDD”) or SAT-based Bounded Model Checking (“BMC”). Default is “BDD”.

boundint, optional

For BMC, the maximum number of steps to be considered. Default is 1000.

find_counterexamplebool, optional

If True and a specification violation is found, a counterexample is produced. Default is False.

print_infobool, optional

If True, information about the verification process is printed. Default is False.

Returns:

bool:

True if the specification is satisfied, False otherwise.

Optional[str]:

A counterexample, if one exists and find_counterexample is True. Otherwise, None.

Module contents