Cited By
View all- Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
Compositional Verification of Simulink Block Diagrams Using tock- and CSP-Prover
Pages 91 - 108
Abstract
The analysis of timed process networks, such as Simulink multi-rate block diagrams, is challenging, particularly for large and complex diagrams whose verification might easily lead to the state explosion problem. For systems of this nature, with an acyclic communication graph, Roscoe and Dathi conceived a compositional deadlock verification strategy by means of local analyses, where only pairs of components need to have their behaviour analysed. Unfortunately, this strategy is restricted to untimed models. In this paper, we extend this strategy to tock-CSP, a dialect of CSP that allows modelling time aspects using a special tock event. This is implemented as a new package in CSP-Prover, a theorem prover for CSP which is itself implemented in Isabelle/HOL. An example demonstrates the benefits of our approach to deadlock analysis of Simulink block diagrams.
References
[1]
Antonino P, Sampaio A, and Woodcock J Jones C, Pihlajasaari P, and Sun J A refinement based strategy for local deadlock analysis of networks of CSP processes FM 2014: Formal Methods 2014 Cham Springer 62-77
[2]
Baxter J, Ribeiro P, and Cavalcanti A Sound reasoning in tock-CSP Acta Inf. 2022 59 125-162
[3]
Bernard, R., Aubert, J., Bieber, P., Merlini, C., Metge, S.: Experiments in model-based safety analysis: flight controls. In: 1st IFAC Workshop on Dependable Control of Discrete Systems (2007)
[4]
Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems, pp. 129–138. LCTES 2012, Association for Computing Machinery, New York, NY, USA (2012).
[5]
Chen C and Dong JS Liu Z and He J Applying timed interval calculus to Simulink diagrams Formal Methods and Software Engineering 2006 Heidelberg Springer 74-93
[6]
Demarchi, F.L.: Modeling and Identification of a Fly-by-Wire Control System. Thesis of master in science, Aeronautical Institute of Technology, São José dos Campos (2005)
[7]
Didier A and Mota A Gheyi R and Naumann D Identifying hardware failures systematically Formal Methods: Foundations and Applications 2012 Berlin Heidelberg, Berlin, Heidelberg Springer 115-130
[8]
Farias A, Mota A, and Sampaio A Compositional abstraction of CSPZ processes J. Braz. Comput. Soc. 2008 14 2 23-44
[9]
Gibson-Robinson T, Armstrong P, Boulgakov A, and Roscoe AW Ábrahám E and Havelund K FDR3 — a modern refinement checker for CSP Tools and Algorithms for the Construction and Analysis of Systems 2014 Heidelberg Springer 187-201
[10]
Gigante G and Pascarella D Margaria T and Steffen B Formal methods in avionic software certification: the DO-178C perspective Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies 2012 Heidelberg Springer 205-215
[11]
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978).
[12]
Isobe, Y., Roggenbach, M.: User guide CSP-prover (2004)
[13]
Isobe, Y., Roggenbach, M., Gruner, S.: Extending CSP-Prover by deadlock-analysis: towards the verification of systolic arrays (2005)
[14]
Jesus J, Mota A, Sampaio A, and Grijo L Qin S and Qiu Z Architectural verification of control systems using CSP Formal Methods and Software Engineering 2011 Heidelberg Springer 323-339
[15]
Mathworks: Simulink User’s Guide. The MathWorks, Inc. (2008). www.mathworks.com
[16]
Mathworks: Simulink Validation and Verification 2 User’s Guide. The MathWorks, Inc. (2008). www.mathworks.com
[17]
Mathworks: Simulink Design Verifier User’s Guide. The MathWorks, Inc. (2019). https://www.mathworks.com/help/pdf_doc/sldv/index.html
[18]
Mota, A., Farias, A., Sampaio, A.: Efficient analysis of infinite CSPZ processes. In: Workshop de Métodos Formais (2002)
[19]
Mota A, Jesus J, Gomes A, Ferri F, and Watanabe E Schoitsch E Evolving a safe system design iteratively Computer Safety, Reliability, and Security 2010 Heidelberg Springer 361-374
[20]
Mota, A., Sampaio, A., Borba, P.: Model checking CSPZ: techniques to overcome state explosion. Sociedade Brasileira de Computação (2002)
[21]
Ogata K Modern Control Engineering 1997 Englewood Cliffs, NJ Prentice-Hall
[22]
Paulson, L.C.: Isabelle: a generic theorem prover. J. Autom. Reasoning 5 (1994)
[23]
Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall PTR (1997)
[24]
Roscoe AW and Dathi N The pursuit of deadlock freedom Inf. Comput. 1987 75 3 289-327
Index Terms
- Compositional Verification of Simulink Block Diagrams Using tock- and CSP-Prover
Index terms have been assigned to the content through auto-classification.
Recommendations
Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem proving
AbstractCompositional deadlock analysis of process networks is a well-known challenge. We propose a compositional deadlock analysis strategy for timed process networks, more specifically, those obtained from Simulink multi-rate block diagrams. We handle ...
Programming and verifying a declarative first-order prover in Isabelle/HOL
We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
Reachability analysis using multiway decision graphs in the HOL theorem prover
SAC '08: Proceedings of the 2008 ACM symposium on Applied computingIn this paper, all the necessary infrastructure is provided to define a state exploration approach within the HOL theorem prover. While related work has tackled the same problem by representing primitive Binary Decision Diagram (BDD) operations as ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Dec 2022
153 pages
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2022.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 06 December 2022
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 21 Nov 2024
Other Metrics
Citations
Cited By
View all- Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in