Formal Verification

26 Oct 2014
by admin
Comments are closed

Formal verification is the name of applying mathematical techniques in order to prove or disprove the correctness of a system against an intended functional behaviour. BlokIDE integrates with formal verifiers and model checkers for ensured correct functional behaviour.

Related Publications

  • [DOI] L. H. Yoong, P. S. Roop, V. Vyatkin, and Z. Salcic, “A synchronous approach for IEC 61499 function block implementation,” Computers, ieee transactions on, vol. 58, iss. 12, pp. 1599-1614, 2009.
    author = {Yoong, Li Hsien and Roop, P.S. and Vyatkin, V. and Salcic, Z.},
    doi = {10.1109/TC.2009.128},
    interhash = {7701d7926a99dfc6dd92c55cf31f7ed6},
    intrahash = {7319a5e0629c4d7db6198d3831c8cc32},
    issn = {0018-9340},
    journal = {Computers, IEEE Transactions on},
    month = {December},
    number = 12,
    pages = {1599 -1614},
    title = {A Synchronous Approach for {IEC} 61499 Function Block Implementation},
    volume = 58,
    year = 2009
  • R. Sinha, “Automated techniques for formal verification of SoCs,” PhD Thesis, 2009.
    author = {Sinha, Roopak},
    interhash = {93df67ff37b3f0c56f579d083e6aabee},
    intrahash = {07af02324572749646f103e4aff789d4},
    publisher = [email protected]},
    school = {The University of Auckland},
    title = {Automated techniques for formal verification of {S}o{C}s},
    url = {},
    year = 2009
  • [DOI] L. H. Yoong and P. S. Roop, “Verifying IEC 61499 function blocks using Esterel,” Embedded systems letters, ieee, vol. 2, iss. 1, pp. 1-4, 2010.
    author = {Yoong, Li Hsien and Roop, P.S.},
    doi = {10.1109/LES.2010.2042275},
    interhash = {29d6d03705d48568ac075c9b7215c25f},
    intrahash = {792128d9ac2dd9d087eb758dd234f17c},
    issn = {1943-0663},
    journal = {Embedded Systems Letters, IEEE},
    month = {March},
    number = 1,
    pages = {1 -4},
    title = {Verifying {IEC} 61499 Function Blocks Using {E}sterel},
    volume = 2,
    year = 2010
  • [DOI] S. A. Ali, P. s. Roop, I. Warren, and Z. E. Bhatti, “Unified management of control flow and data mismatches in web service composition,” in Service oriented system engineering (sose), 2011 ieee 6th international symposium on, 2011, pp. 93-101.
    abstract = {The two main aspects of the web service composition problem are control flow and data mismatches. Several approaches have been reported in the literature to tackle the former; while the latter, and equally relevant aspect for the correct compositional behavior, has either been ignored or addressed to a very limited extent. This paper describes a formal approach based on model checking, that guarantees the correct interaction of services in a composition by managing control flow and resolving data mismatches at semantic, syntactic and structural levels, in a unified manner. A tableau based algorithm is used to generate and explore compositions in a goal-directed fashion, that proves or disproves the existence of a service orchestrator. Successful synthesis of the orchestrator confirms that the required functionality is realizable. Data models to detect and resolve data mismatches are generated using WSDL documents and regular expressions. Experimental results provide strong testimony that the approach can be effectively applied in a practical setting.},
    author = {Ali, Syed Adeel and Roop, Partha s. and Warren, Ian and Bhatti, Zeeshan E.},
    booktitle = {Service Oriented System Engineering (SOSE), 2011 IEEE 6th International Symposium on},
    doi = {10.1109/SOSE.2011.6139097},
    interhash = {3c1a596138d7838b8d176c94c93619c9},
    intrahash = {b9cd8078a61933815c14dca31086401c},
    month = dec,
    pages = {93-101},
    title = {Unified management of control flow and data mismatches in web service composition},
    year = 2011
  • [DOI] Z. E. Bhatti, R. Sinha, and P. S. Roop, “Observer based verification of iec 61499 function blocks,” in Industrial informatics (indin), 2011 9th ieee international conference on, 2011, pp. 609-614.
    abstract = {IEC 61499 is an international standard for designing Industrial Process Control Systems using artefacts such as Function Blocks and Execution Control Charts. The existing approaches towards formal verification of function blocks lack the natural expression for specifying the system properties. We suggest an approach for performing formal verification of IEC 61499 designs using observers expressed as function blocks. This method provides the IEC 61499 designer with an intuitive way of expressing system properties and also makes the verification result easier to map to the original design. We have implemented two different algorithms, a tableau based CTL model checker and a reachability analyzer, to support the verification of observers. Experimental evaluation over a range of benchmarks have shown better performance as compared to Esterel based verification in terms of computation time.},
    author = {Bhatti, Zeeshan E. and Sinha, Roopak and Roop, Partha S.},
    booktitle = {Industrial Informatics (INDIN), 2011 9th IEEE International Conference on},
    doi = {10.1109/INDIN.2011.6034948},
    interhash = {1eb4e671a535d1a152b42c3ed761ad7c},
    intrahash = {5c15adece4d288cfa44d4554d30b91cc},
    month = {July},
    pages = {609-614},
    title = {Observer based verification of IEC 61499 function blocks},
    year = 2011
TimeMe © 2017