Browsing by Author "Belli, F."

Now showing 1 - 15 of 15

Citation Count: 6
The 1st workshop on model-based verification & validation: Directed acyclic graph modeling of security policies for firewall testing
(2009) Tuglular, T.; Kaya, Ö.; Müftüoǧlu, C.A.; Belli, F.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
Currently network security of institutions highly depend on firewalls, which are used to separate untrusted network from trusted one by enforcing security policies. Security policies used in firewalls are ordered set of rules where each rule is represented as a predicate and an action. This paper proposes modeling of firewall rules via directed acyclic graphs (DAG), from which test cases can be automatically generated for firewall testing. The approach proposed follows test case generation algorithm developed for event sequence graphs. Under a local area network setup with the aid of a specifically developed software for this purpose, generated test cases are converted to network test packets, test packets are sent to the firewall under test (FUT), and sent packets are compared with passed packets to determine test result. © 2009 IEEE.
Citation Count: 8
Event-based input validation using design-by-contract patterns
(2009) Tuglular, T.; Muftuoglu, C.A.; Belli, F.; Linschulte, M.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
This paper proposes an approach for validation of numerical inputs based on graphical user interfaces (GUI) that are modeled and specified by event sequence graphs (ESG). For considering complex structures of input data, ESGs are augmented by decision tables and patterns of design by contract (DbC). The approach is evaluated by experiments on boundary overflows, which occur when input values violate the range of specified values. Furthermore, a tool is presented that implements our approach enabling a semiautomatically detection of boundary overflow errors and suggesting correction steps based on DbC. © 2009 IEEE.
Citation Count: 4
GUI-based testing of boundary overflow vulnerability
(2009) Tuglular, T.; Muftuoglu, C.A.; Kaya, O.; Belli, F.; Linschulte, M.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
Boundary overflows are caused by violation of constraints, mostly limiting the range of internal values of a program, and can be provoked by an intruder to gain control of or access to stored data. In order to countermeasure this well-known vulnerability issue, this paper focuses on input validation of graphical user interfaces (GUI). The approach proposed generates test cases for numerical inputs based on GUI specification through decision tables. If boundary overflow error(s) are detected, the source code will be analyzed to localize and correct the encountered error(s) automatically. © 2009 IEEE.
Citation Count: 1
Karar Tablosu Destekli Olay Sira Çizgeleri Temelli Sinama Durum Üretim Arac
(CEUR-WS, 2016) Belli, F.; Linschulte, M.; Tuǧlular, T.; Tuğlular, Tuğkan
[No abstract available]
Model based testing of VHDL programs
(IEEE Computer Society, 2015) Ayav, T.; Tuglular, T.; Belli, F.; Tuğlular, Tuğkan; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
VHDL programs are often validated by means of test benches constructed from formal system specification. To include real-time properties of VHDL programs, the proposed approach first transforms them to concurrently running network of timed automata and then performs model checking on properties taken from the specification. Counterexamples generated by the model checker are used to form a test bench. The approach is validated by a case study composed of a nontrivial application running on a microprocessor. As presented, the approach enables testing both hardware and software at once. © 2015 IEEE.
Model based testing of VHDL programs
(IEEE Computer Society, 2015) Ayav, T.; Tuglular, T.; Belli, F.; Tuğlular, Tuğkan; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
VHDL programs are often validated by means of test benches constructed from formal system specification. To include real-time properties of VHDL programs, the proposed approach first transforms them to concurrently running network of timed automata and then performs model checking on properties taken from the specification. Counterexamples generated by the model checker are used to form a test bench. The approach is validated by a case study composed of a nontrivial application running on a microprocessor. As presented, the approach enables testing both hardware and software at once. © 2015 IEEE.
Citation Count: 3
Model-based contract testing of graphical user interfaces
(Maruzen Co., Ltd., 2015) Tuglular, T.; Muftuoglu, A.; Belli, F.; Linschulte, M.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
Graphical User Interfaces (GUIs) are critical for the security, safety and reliability of software systems. Injection attacks, for instance via SQL, succeed due to insufficient input validation and can be avoided if contract-based approaches, such as Design by Contract, are followed in the software development lifecycle of GUIs. This paper proposes a model-based testing approach for detecting GUI data contract violations, which may result in serious failures such as system crash. A contract-based model of GUI data specifications is used to develop test scenarios and to serve as test oracle. The technique introduced uses multi terminal binary decision diagrams, which are designed as an integral part of decision tableaugmented event sequence graphs, to implement a GUI testing process. A case study, which validates the presented approach on a port scanner written in Java programming language, is presented. Copyright © 2015 The Institute of Electronics, Information and Communication Engineers.
Citation Count: 62
Model-based mutation testing - Approach and case studies
(Elsevier B.V., 2016) Belli, F.; Budnik, C.J.; Hollmann, A.; Tuglular, T.; Wong, W.E.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
This paper rigorously introduces the concept of model-based mutation testing (MBMT) and positions it in the landscape of mutation testing. Two elementary mutation operators, insertion and omission, are exemplarily applied to a hierarchy of graph-based models of increasing expressive power including directed graphs, event sequence graphs, finite-state machines and statecharts. Test cases generated based on the mutated models (mutants) are used to determine not only whether each mutant can be killed but also whether there are any faults in the corresponding system under consideration (SUC) developed based on the original model. Novelties of our approach are: (1) evaluation of the fault detection capability (in terms of revealing faults in the SUC) of test sets generated based on the mutated models, and (2) superseding of the great variety of existing mutation operators by iterations and combinations of the two proposed elementary operators. Three case studies were conducted on industrial and commercial real-life systems to demonstrate the feasibility of using the proposed MBMT approach in detecting faults in SUC, and to analyze its characteristic features. Our experimental data suggest that test sets generated based on the mutated models created by insertion operators are more effective in revealing faults in SUC than those generated by omission operators. Worth noting is that test sets following the MBMT approach were able to detect faults in the systems that were tested by manufacturers and independent testing organizations before they were released. © 2016 Elsevier B.V. All rights reserved.
Model-based selective layer-centric testing
(Information Processing Society of Japan, 2018) Belli, F.; Dincer, N.G.; Linschulte, M.; Tuglular, T.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
Model-based testing of large systems usually requires decomposition of the model into hierarchical submodels for generating test sequences, which fulfills the goals of module testing, but not those of system testing. System testing requires test sequences be generated from a fully resolved model, which necessitates refining the toplevel model, that is, by replacing its elements with submodels they represent. If the depth of model hierarchy is high, the number of test sequences along with their length increases resulting in high test costs. For solving this conflict, a novel approach is introduced that generates test sequences based on the top-level model and replaces elements of these sequences by corresponding, optimized test sequences generated by the submodels. To compensate the shortcoming at test accuracy, the present approach selects components that have lowering impact on the overall system reliability. The objective is to increase the reliabilities of these critical components by intensive testing and appropriate correction which, as a consequence, also increases the overall reliability at less test effort without losing accuracy. An empirical study based on a large web-based commercial system is performed to validate the approach and analyze its characteristics, and to discuss its strengths and weaknesses. © 2018 Information Processing Society of Japan.
Neden-Sonuç Çizgelerinden Test Girilerinin Oluturulmas
(CEUR-WS, 2016) Kavzak, D.; Ayav, T.; Belli, F.; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
Cause-effect graphing is a well-known requirement based testing technique. However, since it was introduced by Myers in 1979, there seems not to have been any suffciently comprehensive studies to generate test cases from these graphs. This paper proposes to convert cause-effect graphs into Boolean expressions and find out the test cases using test input generation techniques for Boolean expressions, such as MI, MAX-A and CUTPNFP. Mutation analysis is used to compare the fault detection capabilities of these techniques and the results are also compared to the Myers' original test generation technique.
Citation Count: 3
Protocol-based testing of firewalls
(2009) Tuglular, T.; Belli, F.; Tuğlular, Tuğkan; Bilgisayar Mühendisliği Bölümü
A firewall is the most important tool of network security defense. Its proper functioning is critical to the network it protects. Therefore a firewall should be tested rigorously with respect to its implemented network protocols and security policy specification. We propose a combined approach for test case generation to uncover errors both in firewall software and in its configuration. In the proposed approach, abstract test cases are generated by mutating event sequence graph model of chosen network protocol and filled with values from policy specification by using equivalence partitioning and boundary value analysis. A case study is presented to validate the presented approach. © 2009 IEEE.
Citation Count: 8
Test input generation from cause–effect graphs
(Springer, 2021) Kavzak Ufuktepe, D.; Ayav, T.; Belli, F.; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
Cause–effect graphing is a well-known requirement-based and systematic testing method with a heuristic approach. Since it was introduced by Myers in 1979, there have not been any sufficiently comprehensive studies to generate test inputs from these graphs. However, there exist several methods for test input generation from Boolean expressions. Cause–effect graphs can be more convenient for a wide variety of users compared to Boolean expressions. Moreover, they can be used to enforce common constraints and rules on the system variables of different expressions of the system. This study proposes a new mutant-based test input generation method, Spectral Testing for Boolean specification models based on spectral analysis of Boolean expressions using mutations of the original expression. Unlike Myers’ method, Spectral Testing is an algorithmic and deterministic method, in which we model the possible faults systematically. Furthermore, the conversion of cause–effect graphs between Boolean expressions is explored so that the existing test input generation methods for Boolean expressions can be exploited for cause–effect graphing. A software is developed as an open-source extendable tool for generating test inputs from cause–effect graphs by using different methods and performing mutation analysis for quantitative evaluation on these methods for further analysis and comparison. Selected methods, MI, MAX-A, MUTP, MNFP, CUTPNFP, MUMCUT, Unique MC/DC, and Masking MC/DC are implemented together with Myers’ technique and the proposed Spectral Testing in the developed tool. For mutation testing, 9 common fault types of Boolean expressions are modeled, implemented, and generated in the tool. An XML-based standard on top of GraphML representing a cause–effect graph is proposed and is used as the input type to the approach. An empirical study is performed by a case study on 5 different systems with various requirements, including the benchmark set from the TCAS-II system. Our results show that the proposed XML-based cause–effect graph model can be used to represent system requirements. The developed tool can be used for test input generation from proposed cause–effect graph models and can perform mutation analysis to distinguish between the methods with respect to the effectiveness of test inputs and their mutant kill scores. The proposed Spectral Testing method outperforms the state-of-the-art methods in the context of critical systems, regarding both the effectiveness and mutant kill scores of the generated test inputs, and increasing the chances of revealing faults in the system and reducing the cost of testing. Moreover, the proposed method can be used as a separate or complementary method to other well-performing test input generation methods for covering specific fault types. © 2021, The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature.
Citation Count: 2
Towards test case generation for synthesizable VHDL programs using model checker
(2010) Ayav, T.; Tuglular, T.; Belli, F.; Tuğlular, Tuğkan; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
VHDL programs are often tested by means of simulations, relying on test benches written intuitively. In this paper, we propose a formal approach to construct test benches from system specification. To consider the real-time properties of VHDL programs, we first transform them to timed automata and then perform model checking against the properties designated from the specification. Counterexamples returned from the model checker serve as a basis of test cases, i.e., they are used to form a test bench. The approach is demonstrated and complemented by a simple case study. © 2010 IEEE.
Citation Count: 2
Towards test case generation for synthesizable VHDL programs using model checker
(2010) Ayav, T.; Tuglular, T.; Belli, F.; Tuğlular, Tuğkan; Ayav, Tolga; Bilgisayar Mühendisliği Bölümü
VHDL programs are often tested by means of simulations, relying on test benches written intuitively. In this paper, we propose a formal approach to construct test benches from system specification. To consider the real-time properties of VHDL programs, we first transform them to timed automata and then perform model checking against the properties designated from the specification. Counterexamples returned from the model checker serve as a basis of test cases, i.e., they are used to form a test bench. The approach is demonstrated and complemented by a simple case study. © 2010 IEEE.
Validation of feature-oriented product configurations using event sequence graphs
(CEUR-WS, 2018) Tuğlular, T.; Belli, F.; Öztürk, D.; Tuğlular, Tuğkan
This study attempts to suggest an approach to systematically test potentially very large number of product variants in feature-oriented software. Feature-oriented software forms a popular concept to efficiently realize software reuse. Developing feature-oriented software is well accepted to accomplish software reuse in an efficient way. Developing product variants by exploiting software reuse requires verification of these variants by exploiting test reuse. However, the reuse of tests in the verification of variants is an underworked topic. In this study, we propose a model-based approach to top-down testing of feature-oriented software that does not have dependency or conflict between features. In the case study, event sequence graphs (ESGs) are used to model the software under consideration and then to generate test cases for positive and negative testing. The generated tests are executed via SahiPro web test automation tool, of which scripts are also automatically generated from ESGs.