publications | Chukri Soueidi

You can also check my publications on Google Scholar.

2023

FASE 23
Opportunistic Monitoring of Multithreaded Programs

Chukri Soueidi, Antoine El-Hokayem, and Yliès Falcone

In Fundamental Approaches to Software Engineering - 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, 2023

Abs Bib link

We introduce a generic approach for monitoring multithreaded programs online leveraging existing runtime verification (RV) techniques. In our setting, monitors are deployed to monitor specific threads and only exchange information upon reaching synchronization regions defined by the program itself. They use the opportunity of a lock in the program, to evaluate information across threads. As such, we refer to this approach as opportunistic monitoring. By using the existing synchronization, our approach reduces additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict. We utilize a textbook example of readers-writers to show how opportunistic monitoring is capable of expressing specifications on concurrent regions. We also present a preliminary assessment of the overhead of our approach and compare it to classical monitoring showing that it scales particularly well with the concurrency present in the program.
@inproceedings{DBLP:conf/fase/SoueidiEF23, author = {Soueidi, Chukri and El{-}Hokayem, Antoine and Falcone, Yli{\`{e}}s}, editor = {Lambers, Leen and Uchitel, Sebasti{\'{a}}n}, title = {Opportunistic Monitoring of Multithreaded Programs}, booktitle = {Fundamental Approaches to Software Engineering - 26th International Conference, {FASE} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 22-27, 2023, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13991}, pages = {173--194}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-30826-0\_10}, doi = {10.1007/978-3-031-30826-0\_10}, timestamp = {Sat, 29 Apr 2023 19:25:03 +0200}, biburl = {https://dblp.org/rec/conf/fase/SoueidiEF23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
SPIN 23
Sound Concurrent Traces for Online Monitoring

Chukri Soueidi, and Yliès Falcone

In Model Checking Software - 29th International Symposium, SPIN 2023, Co-located with the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 26–27, 2023, Proceedings, 2023

Abs Bib link

Monitoring concurrent programs typically rely on collecting traces to abstract program executions. However, existing approaches targeting general behavioral properties are either not tailored for online monitoring, are no longer maintained, or implement naive instrumentation that often leads to unsound verdicts. We first define the notion of when a trace is representative of a concurrent execution. We then present a non-blocking vector clock algorithm to collect sound concurrent traces on the fly reflecting the partial order between events. Moreover, concurrent events in the representative trace pose a soundness problem for monitors synthesized from total order formalisms. For this, we extract a causal dependence relation from the monitor to check if the trace has the needed orderings and define the conditions to decide at runtime when a collected trace is monitorable. We implement our contributions in a tool, FACTS, which instruments programs compiling to Java bytecode, constructs sound representative traces, and warns the monitor about non-monitorable traces. We evaluate our work and compare it with existing approaches.
@inproceedings{10.1007/978-3-031-32157-3_4, author = {Soueidi, Chukri and Falcone, Yli{\`e}s}, editor = {Caltais, Georgiana and Schilling, Christian}, title = {Sound Concurrent Traces for Online Monitoring}, booktitle = {Model Checking Software - 29th International Symposium, SPIN 2023, Co-located with the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 26–27, 2023, Proceedings}, year = {2023}, publisher = {Springer Nature Switzerland}, address = {Cham}, pages = {59--80}, isbn = {978-3-031-32157-3}, doi = {10.1007/978-3-031-32157-3_4}, url = {https://doi.org/10.1007/978-3-031-32157-3_4}, }
ISSRE 23
Dynamic Program Analysis with Flexible Instrumentation and Complex Event Processing

Chukri Soueidi, Yliès Falcone, and Sylvain Hallé

In The 34th IEEE International Symposium on Software Reliability Engineering (ISSRE’23), 2023

Abs Bib link

This paper presents a flexible and modular approach to dynamic program analysis for JVM-based languages, aiming to address the limitations of existing tools. These limitations include the inability to tailor analyses, limited expressiveness, interference from simultaneous analyses, and lack of reusability due to tightly-coupled instrumentation and analysis. The proposed solution decouples these two processes using BISM, a lightweight instrumentation language, and BeepBeep, a complex event processing engine. This novel combination enhances expressiveness, promotes reusability, allows simultaneous and independent analyses, and integrates seamlessly into JVM-based projects. Various analyses such as monitoring, profiling, coverage measurement, and complex event generation are demonstrated, showcasing the approach’s flexibility.
@inproceedings{soueidi2023dynamic, title = {Dynamic Program Analysis with Flexible Instrumentation and Complex Event Processing}, author = {Soueidi, Chukri and Falcone, Yli\`{e}s and Hall\'{e}, Sylvain}, booktitle = {The 34th IEEE International Symposium on Software Reliability Engineering (ISSRE'23)}, pages = {742--751}, year = {2023}, organization = {IEEE Computer Society} }
RV 23
Bridging the Gap: A Focused DSL for RV-Oriented Instrumentation with BISM

Chukri Soueidi, and Yliès Falcone

In Proceedings of the 23rd International Conference on Runtime Verification, 2023

Abs Bib link

We present a novel instrumentation language for BISM, a lightweight bytecode-level instrumentation tool for JVM languages. The new DSL aims to simplify the instrumentation process, making it more accessible to a wider user base. It employs an intuitive syntax, directly mapping to the key requirements of program instrumentation for runtime verification. It enhances productivity by eliminating boilerplate code and low-level details, while also supporting code generation and collaboration. The DSL balances expressiveness and abstraction, bridging the gap between domain experts and the complexities of instrumentation specification.
@inproceedings{soueidi2023bridging, title = {Bridging the Gap: A Focused DSL for RV-Oriented Instrumentation with BISM}, author = {Soueidi, Chukri and Falcone, Yli\`{e}s}, booktitle = {Proceedings of the 23rd International Conference on Runtime Verification}, year = {2023}, organization = {Springer}, pages = {327--338}, address = {Thessaloniki, Greece}, url = {https://link.springer.com/chapter/10.1007/978-3-031-44267-4_17} }
RV 23
Instrumentation for RV: From Basic Monitoring to Advanced Use Cases

Chukri Soueidi, and Yliès Falcone

In Proceedings of the 23rd International Conference on Runtime Verification, 2023

Abs Bib link

Instrumentation is crucial in Runtime Verification because it should ensure that monitors are fed with relevant and accurate information about the executing program under monitoring. While expressive instrumentation is desirable to handle any possible monitoring scenario, instrumentation should also efficiently capture the just-needed information and impact the monitoring program as least as possible. This tutorial comprehensively overviews the instrumentation process and considerations for single and multithreaded programs. We discuss often overlooked aspects in instrumenting multithreaded programs. We also cover metrics for evaluating the efficiency and effectiveness of instrumentation. We use four hands-on use cases to apply the introduced concepts and provide practical guidance on choosing and applying instrumentation for runtime verification.
@inproceedings{soueidi2023instrumentation, title = {Instrumentation for RV: From Basic Monitoring to Advanced Use Cases}, author = {Soueidi, Chukri and Falcone, Yli\`{e}s}, booktitle = {Proceedings of the 23rd International Conference on Runtime Verification}, year = {2023}, eventdate = {3 - 6 October 2023}, address = {Thessaloniki, Greece}, url = {https://link.springer.com/chapter/10.1007/978-3-031-44267-4_23}, }
STTT
Efficient and expressive bytecode-level instrumentation for Java programs

Chukri Soueidi, Marius Monnier, and Yliès Falcone

International Journal on Software Tools for Technology Transfer, 2023

Abs Bib link

We present an efficient and expressive tool for the instrumentation of Java programs at the bytecode level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The instrumentation language is inspired by the aspect-oriented programming paradigm in modularizing instrumentation into separate transformers that encapsulate joinpoint selection and advice inlining, that is the selection of points of interest in the execution and the execution of additional code at these points, respectively. BISM allows capturing joinpoints ranging from bytecode instructions to methods execution and provides comprehensive static and dynamic context information. It runs in two instrumentation modes: build-time and load-time. BISM also provides a mechanism to compose transformers and automatically detect when they interfere on the base program. Transformers in a composition can control the visibility of their advice and other instructions from the base program. We show several example applications for BISM and demonstrate its effectiveness using three experiments: a security scenario, a financial transaction system, and a general runtime verification case. The results show that (i) BISM instrumentation incurs low runtime and memory overheads and (ii) the code produced by BISM performs better than the one produced by existing Java instrumentation tools.
@article{soueidi2023efficient, author = {Soueidi, Chukri and Monnier, Marius and Falcone, Yli{\`e}s}, journal = {International Journal on Software Tools for Technology Transfer}, pages = {1--27}, year = {2023}, publisher = {Springer}, url = {https://link.springer.com/article/10.1007/s10009-023-00708-z}, doi = {10.1007/s10009-023-00708-z} }
Leveraging Runtime Verification for the Monitoring of Digital Twins

Sylvain Hallé, Chukri Soueidi, and Yliès Falcone

In Preproceedings of the Workshop on Applications of Formal Methods and Digital Twins, Mar 2023

Co-located with the 25th International Symposium on Formal Methods

Abs link

The paper considers the problem of discovering divergences between the actions of a digital twin and those of its real-world counterpart. It observes the similarities between this problem and an existing field of formal methods called Runtime Verification (RV), and suggests leveraging and adapting RV techniques to this effect. Concretely, three important aspects of the problem are identified and for which both theoretical and practical challenges must be addressed.
EDOC 23

Monitoring Business Process Compliance Across Multiple Executions with Stream Processing

Chukri Soueidi, Yliès Falcone, and Sylvain Hallé

In Proceedings of the 27th International EDOC Conference (EDOC 2023): Enterprise Design, Operations, and Computing, Mar 2023

To appear

Abs

Compliance checking is the operation that consists of assessing whether every execution trace of a business process satisfies a given correctness condition. The paper introduces the notion of hyperquery, which is a calculation that involves multiple traces from a log at the same time. A particular case of hyperquery is a hypercompliance condition, which is a correctness requirement that involves the whole log instead of individual process instances. Examples of hyperqueries are given for a few representative scenarios. A formalization of hyperqueries is presented, along with a number of elementary operations to express hyperqueries on arbitrary logs. An implementation of these concepts in an event stream processing engine allows users to concretely evaluate hyperqueries in real time.

2022

SAC-SVT

Capturing program models with BISM

Chukri Soueidi, and Yliès Falcone

In SAC ’22: The 37th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, April 25 - 29, 2022, Mar 2022

Abs Bib link

In this paper, we present an extension of the Java bytecode instrumentation tool BISM that captures and prepares a model that abstracts the program behavior at the intra-procedural level. We analyze program methods we are interested in monitoring and construct a control-flow graph automaton where the states represent actions of the program that produce events. Directed towards monitoring general behavioral properties at runtime, the resulting model is presented for the users to write static analyzers and combine both static and runtime verification.

@inproceedings{DBLP:conf/sac/SoueidiF22,
  author = {Soueidi, Chukri and Falcone, Yli{\`{e}}s},
  editor = {Hong, Jiman and Bures, Miroslav and Park, Juw Won and Cern{\'{y}}, Tom{\'{a}}s},
  title = {Capturing program models with {BISM}},
  booktitle = {{SAC} '22: The 37th {ACM/SIGAPP} Symposium on Applied Computing, Virtual
                   Event, April 25 - 29, 2022},
  pages = {1857--1861},
  publisher = {{ACM}},
  year = {2022},
  url = {https://doi.org/10.1145/3477314.3507239},
  doi = {10.1145/3477314.3507239},
  timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
  biburl = {https://dblp.org/rec/conf/sac/SoueidiF22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

VSTTE
Residual Runtime Verification via Reachability Analysis

Chukri Soueidi, and Yliès Falcone

In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Mar 2022

Abs Bib link

We leverage static verification to reduce monitoring overhead when runtime verifying a property. We present a sound and efficient analysis to statically find safe execution paths in the control flow at the intra-procedural level of programs. Such paths are guaranteed to preserve the monitored property and thus can be ignored at runtime. Our analysis guides an instrumentation tool to select program points that should be observed at runtime. The monitor is left to perform residual runtime verification for parts of the program that the analysis could not statically prove safe. Our approach does not depend on dataflow analysis, thus separating the task of residual analysis from static analysis; allowing for seamless integration with many RV frameworks and development pipelines. We implement our approach within BISM, which is a recent tool for bytecode-level instrumentation of Java programs. Our experiments on the DaCapo benchmark show a reduction in instrumentation points by a factor of 2.5 on average (reaching 9), and accordingly, a reduction in the number of runtime events by a factor of 1.8 on average (reaching 6).
@inproceedings{DBLP:conf/vstte/SoueidiF22, author = {Soueidi, Chukri and Falcone, Yli{\`{e}}s}, editor = {Lal, Akash and Tonetta, Stefano}, title = {Residual Runtime Verification via Reachability Analysis}, booktitle = {Verified Software. Theories, Tools and Experiments - 14th International Conference, {VSTTE} 2022, Trento, Italy, October 17-18, 2022}, series = {Lecture Notes in Computer Science}, volume = {13800}, pages = {148--166}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-25803-9\_9}, doi = {10.1007/978-3-031-25803-9\_9}, timestamp = {Sat, 25 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/vstte/SoueidiF22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }

2020

RV
BISM: Bytecode-Level Instrumentation for Software Monitoring

Chukri Soueidi, Ali Kassem, and Yliès Falcone

In Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings, Mar 2020

Abs Bib link

BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool which features an expressive high-level control-flow-aware instrumentation language. The language follows the aspect-oriented programming paradigm by adopting the joinpoint model, advice inlining, and separate instrumentation mechanisms. BISM provides joinpoints ranging from bytecode instruction to method execution, access to comprehensive context information, and instrumentation methods. BISM runs in two modes: build-time and load-time. We demonstrate BISM effectiveness using two experiments: a security scenario and a general runtime verification case. The results show that BISM instrumentation incurs low runtime and memory overheads.
@inproceedings{DBLP:conf/rv/SoueidiKF20, author = {Soueidi, Chukri and Kassem, Ali and Falcone, Yli{\`{e}}s}, editor = {Deshmukh, Jyotirmoy and Nickovic, Dejan}, booktitle = {Runtime Verification - 20th International Conference, {RV} 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12399}, pages = {323--335}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-60508-7\_18}, doi = {10.1007/978-3-030-60508-7\_18}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/rv/SoueidiKF20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

2019

AUB

Behavioural modeling and abstraction of concurrent programs.

Chukri Soueidi

Mar 2019

Abs link PDF

We address the problem of modeling, analyzing, and repairing finite-state and infinite-state concurrent programs. We define a textual notation for concurrent programs and implement it in the Eshmun tool. For finite-state programs, we automatically generate Kripke structures (transition diagrams) from the program text. This structure can then be model checked and repaired using Eshmun facilities. The resulting repair can then be used to guide the designer in fixing the program itself. For infinite-state programs, we define the notion of a finitely-representable infinite-state Kripke structure, and we provide a semi-automatic method for generating such a structure from an infinite-state concurrent program. This structure models the behavior of the infinite state concurrent program. We label the states of the Kripke structure with state predicates, and the transitions with preconditions P and postconditions Q. Each transition τ then generates a Hoare triple [P] τ [Q] which we verify using the Z3 SMT solver. Hoare triples that are not valid must be repaired. When all triples are valid, we model check to determine if the required properties hold. If the model check fails, more repair is needed. If the model check succeeds, we can semi-automatically extract a correct infinite state concurrent program.

2015

PACKT

Microsoft Azure Storage Essentials

Chukri Soueidi

Mar 2015

Abs Bib link

@article{soueidi_2015,
  title = {Microsoft Azure Storage Essentials},
  publisher = {Packt Publishing},
  author = {Soueidi, Chukri},
  year = {2015},
  url = {https://www.packtpub.com/product/microsoft-azure-storage-essentials/9781784396237?utm_source=google&utm_medium=cpc&utm_campaign=18331805515&utm_content=621682243179&utm_term=packt%20books&utm_tm=true}
}