Automatic Generation of Formal BIP Models for C Programs
Authors: 
Qiming Li, Xia Yang, Haiyong Sun, Zhe YanAuthors Info & Claims
Article No.: 52, Pages 1 - 7
Abstract
The BIP model is based on a combinatorial model-checking technique, which decomposes a software system into behavioral components, interaction components and priority rules. It can effectively formalize the description and verification of complex software systems, and is widely used in industry. However, BIP models require manual modeling and rely heavily on professional knowledge, so there are issues related to high cost, low efficiency, and difficulty in guaranteeing model accuracy. In this paper, an automatic BIP model generation method for C programs is proposed, which can automatically extract key program information to build a middle layer Labelled Transition System (LTS) and finally generate a BIP model. This paper further conducts automatic behavioral modeling of a high-performance dynamic memory allocation algorithm and successfully verifies 12 essential security requirements related to the algorithm. Experimental results show that the proposed automatic formal modeling method can effectively reduce manual dependency and improve modeling efficiency, while ensuring the accuracy of the constructed model.
References
[1]
Basu, A., Bozga, M. and Sifakis, J. (2006). Modeling heterogeneous real-time components in BIP. In Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) (pp. 3-12). IEEE.
[2]
Razzaq, S., Zafar, R., Khan, N. A., Butt, A. R. and Mahmood, A. (2016). A novel prosumer-based energy sharing and management (PESM) approach for cooperative demand side management (DSM) in smart grid. Applied Sciences, 6(10), 275.
[3]
Basu, A., Bensalem, B., Bozga, M., Combaz, J., Jaber, M., Nguyen, T. H. and Sifakis, J. (2011). Rigorous component-based system design using the BIP framework. IEEE software, 28(3), 41-48.
[4]
Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T. H. and Peled, D. (2011,). Efficient deadlock detection for concurrent systems. In Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011) (pp. 119-129). IEEE.
[5]
Kulczynski, M., Legay, A., Nowotka, D. and Poulsen, D. B. (2021). Analysis of source code using UPPAAL. arXiv preprint arXiv:2108.02963.
[6]
Byun, M., Lee, Y. and Choi, J. Y. (2020). Analysis of software weakness detection of CBMC based on CWE. In 2020 22nd International Conference on Advanced Communication Technology (ICACT) (pp. 171-175). IEEE.
[7]
Henzinger, T. A., Jhala, R., Majumdar, R. and Sutre, G. (2002). Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 58-70).
[8]
Beyer, D. and Friedberger, K. (2020). Violation Witnesses and Result Validation for Multi-Threaded Programs: Implementation and Evaluation with CPAchecker. In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I 9 (pp. 449-470). Springer International Publishing.
[9]
Bourgos P, Basu A, Bensalem S, (2010). Integrating architectural constraints in application software by source-to-source transformation in bip[R]. Technical Report TR-2011-1, Verimag Research Report.
[10]
Baier, C. and Katoen, J. P. (2008). Principles of model checking. MIT press.
[11]
Antunes, H., Carnielli, W., Kapsner, A. and Rodrigues, A. (2020). Kripke-style models for logics of evidence and truth. Axioms, 9(3), 100.
[12]
Baier, C., de Alfaro, L., Forejt, V. and Kwiatkowska, M. (2018). Model checking probabilistic systems. Handbook of Model Checking, 963-999.
[13]
Masmano, M., Ripoll, I., Crespo, A. and Real, J. (2004). TLSF: A new dynamic memory allocator for real-time systems. In Proceedings. 16th Euromicro Conference on Real-Time Systems, 2004. ECRTS 2004. (pp. 79-88). IEEE.
[14]
Astrauskas, V., Müller, P., Poli, F. and Summers, A. J. (2019). Leveraging Rust types for modular specification and verification. Proceedings of the ACM on Programming Languages, 3(OOPSLA), 1-30.
[15]
Sherwood, T., Perelman, E. and Calder, B. (2001). Basic block distribution analysis to find periodic behavior and simulation points in applications. In Proceedings 2001 International Conference on Parallel Architectures and Compilation Techniques (pp. 3-14). IEEE.
[16]
Beyer, D. (2022). Progress on software verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II (pp. 375-402). Cham: Springer International Publishing.
[17]
Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N. and Zadeck, F. K. (1991). Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS), 13(4), 451-490.
[18]
Lattner, C. (2008, May). LLVM and Clang: Next generation compiler technology. In The BSD conference (Vol. 5, pp. 1-20).
[19]
Wilson, P. R., Johnstone, M. S., Neely, M. and Boles, D. (1995). Dynamic storage allocation: A survey and critical review. In Memory Management: International Workshop IWMM 95 Kinross, UK, September 27–29, 1995 Proceedings (pp. 1-116). Springer Berlin Heidelberg.
[20]
Pnueli, A. (1977, October). The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) (pp. 46-57). IEEE.
[21]
Rescher, N. and Urquhart, A. (2012). Temporal logic (Vol. 3). Springer Science & Business Media.
Index Terms
- Automatic Generation of Formal BIP Models for C Programs
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Automated formal verification of visual modeling languages by model checking
Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling ...
Formal verification of SystemCFLspecifications using SPIN
MINO'06: Proceedings of the 5th WSEAS international conference on Microelectronics, nanoelectronics, optoelectronicsThe formal language SystemCFL is the formalization of SystemC. The language semantics of SystemCFL was formally defined in a standard structured operational semantics (SOS) style. For verification purposes, in this paper, we present an approach to use ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
358 pages
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 21 December 2023
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
CSAE 2023
CSAE 2023: The 7th International Conference on Computer Science and Application Engineering
October 17 - 19, 2023
Virtual Event, China
Acceptance Rates
Overall Acceptance Rate 368 of 770 submissions, 48%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 25Total Downloads
- Downloads (Last 12 months)25
- Downloads (Last 6 weeks)1
Reflects downloads up to 21 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format