Change search
ReferencesLink to record
Permanent link

Direct link
Sound Extraction of Control-Flow Graphs from open Java Bytecode Systems
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6468-1605
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2012 (English)Report (Other academic)
Abstract [en]

Formal verification techniques have been widely deployed as means to ensure the quality of software products. Unfortunately, they suffer with the combinatorial explosion of the state space. That is, programs have a large number of states, sometimes infinite. A common approach to alleviate the problem is to perform the verification over abstract models from the program. Control-flow graphs (CFG) are one of the most common models, and have been widely studied in the past decades. Unfortunately, previous works over modern programming languages, such as Java, have either neglected features that influence the control-flow, or do not provide a correctness argument about the CFG construction. This is an unbearable issue for formal verification, where soundness of CFGs is a mandatory condition for the verification of safety-critical properties. Moreover, one may want to extract CFGs from the available components of an open system. I.e., a system whose at least one of the components is missing. Soundness is even harder to achieve in this scenario, because of the unknown inter-dependences between software components.

In the current work we present a framework to extract control-flow graphs from open Java Bytecode systems in a modular fashion. Our strategy requires the user to provide interfaces for the missing components. First, we present a formal definition of open Java bytecode systems. Next, we generalize a previous algorithm that performs the extraction of CFGs for closed programs to a modular set-up. The algorithm uses the user-provided interfaces to resolve inter-dependences involving missing components. Eventually the missing components will arrive, and the open system will become closed, and can execute. However, the arrival of a component may affect the soundness of CFGs which have been extracted previously. Thus, we define a refinement relation, which is a set of constraints upon the arrival of components, and prove that the relation guarantees the soundness of CFGs extracted with the modular algorithm. Therefore, the control-flow safety properties verified over the original CFGs still hold in the refined model.

We implemented the modular extraction framework in the ConFlEx tool. Also, we have implemented the reusage from previous extractions, to enable the incremental extraction of a newly arrived component. Our technique performs substantial over-approximations to achieve soundness. Despite this, our test cases show that ConFlEx is efficient. Also, the extraction of the CFGs gets considerable speed-up by reusing results from previous analyses.

Place, publisher, year, edition, pages
2012. , 49 p.
Keyword [en]
Software Verification, Static Analysis, Program Models, Compositional Verification
National Category
Computer Systems
Research subject
SRA - E-Science (SeRC)
URN: urn:nbn:se:kth:diva-104076OAI: diva2:562962
Verification of Control-Flow Properties of Programs with Procedures(CVPP)
Swedish eā€Science Research Center

QC 20121029

Available from: 2012-10-29 Created: 2012-10-26 Last updated: 2013-12-13Bibliographically approved

Open Access in DiVA

fulltext(573 kB)189 downloads
File information
File name FULLTEXT03.pdfFile size 573 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
de Carvalho Gomes, PedroPicoco, AttilioGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 265 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 301 hits
ReferencesLink to record
Permanent link

Direct link