OCRA VERSION 2.1.0 (Jul 2, 2021) We are happy to announce the availability of a new version of OCRA. OCRA version 2.1.0 is available from https://es.fbk.eu/tools/ocra/ This is a major release that provides a new time domain Several bugs were also fixed. The main changes are listed below. ---------------------------------------------------------------------- * New features ---------------------------------------------------------------------- o Options: NEW: --ocra-timed New command option to enable timed domain. This new time domain supports only a limited amount of commands. o Input language NEW: clock clock is a new variable type introduced for the timed domain NEW: within[0, n] / within(0, 5] / within[4, +oo) Within is an operator that is used with another temporal operator to restrict the that operator in a closed range (e.g. G p[0, 5] in discrete time means that p holds for 5 steps). This operator can be used in discrete and timed domains. In discrete time it is mandatory to use only finite positive numbers inside the within range, while in timed domain it is permitted use also +oo and parameters as range elements. The "within" operator has 2 different semantics: - in discrete time the operator considers the discrete transitions - in timed domain the operator considers the time elapsed Examples: - always p within [0, 5]; - X within[0, c0]; - F d [3, 15]; - in the future p within[10, +oo) For additional information, please see the user manual. ------------------------------------------------------------------------------- OCRA VERSION 2.0.0 (Jul 28, 2020) We are happy to announce the availability of a new version of OCRA. OCRA version 2.0.0 is available from https://es.fbk.eu/tools/ocra/ This is a major release that provides a major extension of the OCRA language, namely the possibility to parametrize OCRA architectures using parameters to define the number of subcomponents, ports, and more. New commands have been added to validate the contract specification, synthesizing tightened versions and debugging the contracts using input traces. Several bugs were also fixed. The main changes are listed below. ---------------------------------------------------------------------- * New features ---------------------------------------------------------------------- o Input language NEW: parametrized OCRA language: NEW: for iterators Expression that describes indipendents ranges with indexes NEW: big_or operator Operator that contains a for iterator and from the iterators build a concatenations of or expressions. NEW: big_and operator Operator that contains a for iterator and from the iterators build a concatenations of and expressions. NEW: count extension to support iterators Count now can contain for iterators, this allows to expand count expression up to n elements where n can be a parameter. NEW: parametric connection now connections can be defined with an if expression and with iterators NEW: parametric contract contracts now can be defined with an iterator NEW: parametric refinedby refinedby elements can now have iterators on subcomponents contracts NEW: assertions Expression that can be checked as LTL specifications by ocra_check_validation_prop command, can also be used as contract's asumption or guarantee. o Commands: NEW: ocra_instantiate_parametric_arch Instantiate a parametric OSS file. User can both use CSV file or CSV string for the assignment of the architectural parameters NEW: ocra_get_required_arch_params Returns a list of required architectural parameters that should be instantiated in order to go further with the instantiation. NEW: ocra_instantiate_automatically_arch Instantiate a parametric architecture with all possible parameters values NEW: ocra_check_param_refinement Check recursively the component contracts refinement of a parametrized model NEW: ocra_tighten_contract_refinement Tighten a contract refinement Tightening by default is top-down, but with the option -g is possible to do it bottom-up NEW: ocra_debug_property Debugs all unsatisfied proof obbligations and entailment properties For additional information regarding the parametric architecture see the manual in the section: "Parametrized Ocra". Two examples of parametrized architecures can be find in the examples/discrete/SenseSpacecraftRate/ and examples/discrete/air_traffic_control folders. ------------------------------------------------------------------------------- OCRA VERSION 1.4.0 (Jul 17, 2015) We are happy to announce the availability of a new version of OCRA. OCRA version 1.4.0 is available from https://es.fbk.eu/tools/ocra/ This is a major release that provides six new commands, a new port type, handy extensions of the input language, the Mac OS X executable, and several bug fixes. The main changes are listed below. ---------------------------------------------------------------------- * New features ---------------------------------------------------------------------- o Commands NEW: ocra_check_validation_prop Checks validation properties (consistency, possibility, and entailment) defined in an oss file. NEW: ocra_show_property Shows the currently stored properties in an ocra session. NEW: ocra_show_traces Shows the traces generated in an ocra session. NEW: ocra_check_ltlspec_on_trace Checks whether a property is satisfied on a trace. NEW: ocra_compute_fault_tree It provides hierarchical fault tree generation from a contract based decomposition. NEW: option -C It allows to restrict a check to a single contract. Available for ocra_check_refinement, ocra_check_implementation and ocra_check_composite_impl. NEW: option -s Prints a summarized result, to enhance readability. Available for ocra_check_refinement and ocra_check_validation_prop NEW: option -l Set the bound of K-Liveness. Available for ocra_check_implementation and ocra_check_composite_impl. ocra_check_consistency NEW: option -j Performs two new checks. For each contract, checks consistency of the conjunction of its assumption and guarantee. Moreover, for each composite component C, checks consistency among assumption of C and assumptions and guarantees of all subcomponents. o Input language NEW: uninterpreted functions port type A port can now be declared to have function type. NEW: defines Name an expression to make complex contracts more readable. NEW: validation properties New construct to validate the contract refinement. There are three types of validation properties that can be defined: consistency, possibility, and entailment. ---------------------------------------------------------------------- * Archive content ---------------------------------------------------------------------- o NEW: Mac OS X executable o NEW: ocra-mode.el for emacs