Login

Bilal Abed Al Houssein Kanso

Assistant professor
Computer Science - Statistics department - Section V - Nabatiyeh
Speciality: Computer Science
Specific Speciality: Informatique - Méthodes Formelles

Teaching 4 Taught Courses
(2014-2015) Info 203 - Imperative Programming I

BS Computer Sciences

(2014-2015) Info 216 - Imperative programming II

BS Computer Sciences

(2014-2015) Info 327 - Applied database and programming

BS Computer Sciences

(2014-2015) Info 327 - Applied database and programming

BS Computer Sciences

Education
2008 - 2011: PhD

Ecole Centrale Paris
Formal methods

2007 - 2008: Master 2

UFRIMA Joseph Fourier University - Grenoble, France
Formal methods

2003 - 2007: Master 1

Lebanese University

Publications 9 publications
Bilal Kanso, Omar Chbaro Compositional testing for FSM-based models. 2014

The contribution of this paper is threefold: first, it defines a framework for modelling component-based systems, as well as a formalization of integration rules to combine their behavior. This is based on finite state machines (FSM). Second, it studies compositional conformance testing i.e. checking whether an implementation made of conforming components combined with integration operators is conform to its specification. Third, it shows the correctness of the global system can be obtained by testing the components involved into it towards the projection of the global specification on the specifications of the components. This result is useful to build adequate test purposes for testing components taking into account the system where they are plugged in.

M. Aiguier, B. Kanso Logic for complex computing system Scientific Annals of Computer Science journal 2014

In a previous paper [1], we defined both a unified formal framework based on L.-S. Barbosa's components for modeling complex software systems, and a generic formalization of integration rules to combine their behavior. In the present paper, we propose to continue this work by proposing a variant of first-order fixed point modal logic to express both components and systems requirements. We establish the important property for this logic to be adequate with respect to bisimulation. We then study the conditions to be imposed to our logic (characterization of sub-families of formul\ae) to preserve properties along integration operators, and finally show correctness by construction results. The complexity of computing systems results in the definition of formal means to manage their size. To deal with this issue, we propose an abstraction (resp. simulation) of components by components. This enables us to build systems and check their correctness in an incremental way.

Safouan Taha, Jacques Julliand, Frédéric Dadeau, Kalou Cabrera Castillos, Bilal Kanso A Compositional Automata-based Semantics and Preserving Transformation Rules for Testing Property Patterns. FAC journal, Springer 2014

Dwyer et al. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal logics (linear temporal logic, CTL, etc.). This translational semantics suffers from two main issues. It is not easily extensible to other patterns or scopes, and it is not always faithful to the natural semantics. In this article, we propose a compositional automata-based approach defining the semantics of each pattern and each scope by an automaton, after which the semantics is composed. Hence, the semantics is compositional and the language is easily extensible. We compare the two semantics by model checking. In some cases, our semantics reveals a lack of homogeneity within Dwyer et al.’s semantics. Finally, we apply this approach in the context of property-based testing, in order to evaluate the quality of a test suite, by measuring the coverage of the property automaton. To allow the tester to adapt the coverage criteria to its goals, we propose transformation rules over the patterns automata that implement relevant unfolding strategies for loops, or predicates labeling the automata transitions. We illustrate these principles by means of an industrial case study.

B. Kanso et S. Taha Specification of Temporal Properties with OCL Science of Computer Science 2013

The Object Constraint Language (OCL) is widely used to express static constraints on models and object-oriented systems. However, the notion of dynamic constraints, controlling the system behavior over time, has not been natively supported. Such dynamic constraints are necessary to handle temporal and real-time properties of systems. In this paper, we first add a temporal layer to the OCL language, based syntactically on Dwyer et al.'s specification patterns. We enrich it with formal scenario-based semantics and integrate it into the current Eclipse OCL plug-in. Second, we translate, with a compositional approach, OCL temporal properties into finite-state automata and we connect our framework to automatic test generators. This way, we create a bridge linking model driven engineering and usual formal methods.

K. Cabrera Castillos, F. Dadeau, Jacques Jullian, B. Kanso et S. Taha A Compositional Automata-Based Semantics for Property Patterns. 10th International Conference on integrated Formal Methods(iFM’10), springer 2013

Dwyer et al. define a language to specify dynamic properties based on predefined patterns and scopes. To define a property, the user has to choose a pattern and a scope among a limited number of them. Dwyer et al. define the semantics of these properties by translating each composition of a pattern and a scope into usual temporal logics (LTL, CTL, etc.). First, this translational semantics is not compositional and thus not easily extensible to other patterns/scopes. Second, it is not always faithful to the natural semantics of the informal definitions.

Bilal Kanso, Safouan Taha Temporal Constraint Support for OCL Software Language Engineering, Springer 2012

The Object Constraint Language is widely used to express precise and unambiguous constraints on models and object oriented programs. However, the notion of temporal constraints, controlling the system behavior over time, has not been natively supported. Such temporal constraints are necessary to model reactive and real-time systems. Although there are works addressing temporal extensions of OCL, they only bring syntactic extensions without any concrete implementation conforming to the OCL standard. On top of that, all of them are based on temporal logics that require particular skills to be used in practice. In this paper, we propose to fill in both gaps. We first enrich OCL by a pattern-based temporal layer which is then integrated into the current Eclipse’s OCL plug-in. Moreover, the temporal constraint support for OCL, that we define using formal scenario-based semantics, connects to automatic test generators and forms the first step towards creating a bridge linking model driven engineering and usual formal methods.

B. Kanso, M. Aiguier, F. Boulanger et G. Gaston Testing of component- based systems 19th Asia-pacific Software Engineering Conference (APSEC’19), IEEE 2012

In this paper, we pursue our works on generic modeling and testing of component-based systems. Here, we extend our conformance testing theory to the testing of component-based systems. We first show that testing a global system can be done by testing its components thanks to the projection of global behaviors onto local ones. Secondly, based on our projection techniques, we define a framework to build adequate test purposes automatically for testing components in the context of the global system where they are plugged in. The basic idea is to identify from any trace try of the global system, the trace of any component involved in tr. Those projected traces can be then seen as test cases that should be tested on individual components

: M. Aiguier, F. Boulanger et B. Kanso A formal abstract framework for mod- eling and testing complex software-intensive systems. Theoretical Computer Science (TCS) 2011

The contribution of this paper is twofold: first, it defines a unified framework for modelling abstract components, as well as a formalization of integration rules to combine their behaviour. This is based on a coalgebraic definition of components, which is a categorical representation allowing the unification of a large family of formalisms for specifying state-based systems. Second, it studies compositional conformance testing i.e. checking whether an implementation made of correct interacting components combined with integration operators conforms to its specification.

B. Kanso, M. Aiguier, F. Boulanger et A. Touil. Testing of Ab- stract Components. In International Colloquium on Theoretical Aspects of Comput- ing (ICTAC’10), Springer 2010

In this paper, we present a conformance testing theory for Barbosa’s abstract components. We do so by defining a trace model for components from causal transfer functions which operate on data flows at discrete instants. This allows us to define a test selection strategy based on test purposes which are defined as subtrees of the execution tree built from the component traces. Moreover, we show in this paper that Barbosa’s definition of components is abstract enough to subsume a large family of state-based formalisms such as Mealy machines, Labeled Transition Systems and Input/Output Labeled Transition Systems. Hence, the conformance theory presented here is a generalization of the standard theories defined for different state-based formalisms and is a key step toward a theory of the test of heterogeneous systems.