2024-03-29T00:19:36Z
https://zenodo.org/oai2d
oai:zenodo.org:4266976
2020-11-10T22:44:11Z
user-ftsrg
Micskei, Zoltán
Honfi, Dávid
2020-11-10
<p>Software testing is an inevitable part of software development to ensure the quality of the product. Thorough testing of software, however, might consume an significant amount of time and resources. Therefore, already decades ago, research has begun to reduce this effort by automating the process, while improving the efficiency of testing as well. One of the recommended methods is white-box test generation, which uses only the source code to generate test cases. Although there are several types of techniques using this idea - including symbolic execution, search-based testing, and guided random testing - the complexity of real-world software can make their application burdensome. These techniques usually suffer from issues, when the software under test interacts with its environment, structured objects should be created for good coverage, valid test oracles should be guessed, or the size of the program is too large. Furthermore, the use of such advanced techniques is not trivial for ordinary developers or testers due to their underlying complexity, hence the identification of test generation problems can be a difficult task as well. This work empirically evaluates these challenges and addresses some of them by proposing new techniques and tools for white-box test generation.</p>
https://doi.org/10.5281/zenodo.4266976
oai:zenodo.org:4266976
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.4266975
info:eu-repo/semantics/restrictedAccess
software testing
test generation
white-box testing
symbolic execution
empirical study
Evaluating and Improving White-Box Test Generation
info:eu-repo/semantics/doctoralThesis
oai:zenodo.org:7564295
2023-05-11T04:11:43Z
user-ftsrg
Horváth, Benedek
Molnár, Vince
Graics, Bence
Hajdu, Ákos
Ráth, István
Horváth, Ákos
Karban, Robert
Trancho, Gelys
Micskei, Zoltán
2023-01-24
<p>This report is supplementary material to the paper Horváth et al. <em>Pragmatic Verification and Validation of Industrial Executable SysML Models</em>. It provides insights into the transformation rules between SysML and Gamma, both on the conceptual and the technical<br>
level.</p>
https://doi.org/10.5281/zenodo.7564295
oai:zenodo.org:7564295
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.7564294
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
formal verification, model-based systems engineering, model transformation, model checking
Supplementary Material to the Pragmatic Verification and Validation of Industrial Executable SysML Models
info:eu-repo/semantics/technicalDocumentation
oai:zenodo.org:3474274
2020-02-16T15:20:57Z
openaire_data
user-ftsrg
David Honfi
Zoltan Micskei
2019-09-22
<p>We present an approach for automated isolation in white-box test generation. This publication contains the data and the corresponding analysis script written in R.</p>
https://doi.org/10.5281/zenodo.3474274
oai:zenodo.org:3474274
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3457479
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
testing
test generation
white-box
isolation
Automated Isolation for White-box Test Generation
info:eu-repo/semantics/other
oai:zenodo.org:3457480
2020-02-16T15:20:56Z
openaire_data
user-ftsrg
David Honfi
Zoltan Micskei
2019-09-22
<p>We present an approach for automated isolation in white-box test generation. This publication contains the data and the corresponding analysis script written in R.</p>
https://doi.org/10.5281/zenodo.3457480
oai:zenodo.org:3457480
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3457479
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
testing
test generation
white-box
isolation
Automated Isolation for White-box Test Generation
info:eu-repo/semantics/other
oai:zenodo.org:7263707
2022-10-30T02:26:34Z
openaire_data
user-ftsrg
Ádám, Zsófia
Micskei, Zoltán
2022-10-29
<p>Dataset of the Scientific Students’ Association Report titled Abstraction-based Trace Generation to Validate Semantics of Formal Verifiers.</p>
<p>These files contain the validation model test suite and the generated traces. The models and traces are in the format of the Gamma modeling tool.</p>
<p><em>validation-model-suite/model/package<Letter>/model<Number> </em>contains the files for a given model:<br>
- stm.gcd is the statemachine,<br>
- default.ggen (and in Package F also abstraction.ggen) is the Gamma script executing trace generation and the generated traces can be found in the default (and abstraction) directories.<br>
The report of Theta on possible coverage violation is in the traces directory (report.txt).</p>
<p> </p>
<p>The prototype implementation of trace generation can be found at: https://github.com/AdamZsofi/gamma/tree/dev-tracegen</p>
https://doi.org/10.5281/zenodo.7263707
oai:zenodo.org:7263707
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.7263706
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Abstraction-based Trace Generation to Validate Semantics of Formal Verifiers: Validation Model Suite
info:eu-repo/semantics/other
oai:zenodo.org:10256749
2023-12-10T12:45:37Z
openaire_data
user-ftsrg
Szabó, Richárd
Szekeres, Dániel
Nagy, Simon József
Thimár, Zoltán
Majzik, Istvan
Micskei, Zoltán
Vörös, András
2023-12-08
<p>This dataset provides artifacts about an industrial case study of a Steer-by-Wire system. It collects models of the system modeled in the open-source Gamma Statechart Composition Framework. You can find more information about the framework here: <a href="https://github.com/ftsrg/gamma">https://github.com/ftsrg/gamma</a>.</p>
https://doi.org/10.5281/zenodo.10256749
oai:zenodo.org:10256749
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.10256748
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
safety concept
fault tolerance
system architecture
formal verification
steer-by-wire system
Supplementary Material for "Iterative Exploration of Distinct Requirement Violation Scenarios for Fault-tolerant Architectures"
info:eu-repo/semantics/other
oai:zenodo.org:1219261
2020-01-20T13:34:59Z
user-ftsrg
Hajdu, Ákos
Micskei, Zoltán
2018-01-29
<p>Formal verification techniques can check the correctness of systems in a mathematically precise way. Counterexample-Guided Abstraction Refinement (CEGAR) is an automatic algorithm that reduces the complexity of systems by constructing and refining abstractions. CEGAR is a generic approach, having many variants and strategies developed over the years. However, as the variants become more and more advanced, one may not be sure whether the performance of a strategy can be attributed to the strategy itself or to other, unintentional factors. In this paper we perform an experiment by evaluating the performance of different strategies while randomizing certain external factors such as the search strategy and variable naming. We show that randomization introduces a great variation in the output metrics, and that in several cases this might even influence whether the algorithm successfully terminates.</p>
https://doi.org/10.5281/zenodo.1219261
oai:zenodo.org:1219261
eng
Budapest University of Technology and Economics, Department of Measurement and Information Systems
https://doi.org/10.5281/zenodo.1117853
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1219260
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
25th PhD Mini-Symposium, Budapest, Hungary, 29 January 2018
formal verification
cegar
abstraction
theta
randomization
experimental evaluation
A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework
info:eu-repo/semantics/conferencePaper
oai:zenodo.org:1290661
2020-01-20T14:40:40Z
user-ftsrg
Kristóf, Marussy
István, Majzik
2018-06-15
<p>Technical report on the transformation of mission automata to phased-mission systems for the dependability analysis of reconfigurable manufacturing systems.</p>
https://doi.org/10.5281/zenodo.1290661
oai:zenodo.org:1290661
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1290660
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Constructing Phased-Mission Systems for Dependability Analysis of Reconfigurable Production Systems
info:eu-repo/semantics/technicalDocumentation
oai:zenodo.org:3893955
2020-06-15T10:18:22Z
openaire_data
user-ftsrg
Hajdu, Ákos
Micskei, Zoltán
2020-06-15
<p>Supplementary material for the paper "Efficient Strategies for CEGAR-based Model Checking" by Akos Hajdu and Zoltan Micskei. The material includes a detailed report (report.html) and all artifacts to replicate our measurements and analysis (artifact.tar.gz).</p>
<p><em>Version 1.2.0 corresponds to the final, published paper. This version (1.2.1) is a minor update that added two new plots.</em></p>
https://doi.org/10.5281/zenodo.3893955
oai:zenodo.org:3893955
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1252784
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Formal verification
Abstraction
CEGAR
Experimental evaluation
Supplementary Material for the paper "Efficient Strategies for CEGAR-based Model Checking"
info:eu-repo/semantics/other
oai:zenodo.org:3965792
2020-10-20T14:35:04Z
openaire_data
user-ftsrg
Tóth, Tamás
Majzik, István
2020-07-29
<p>The tool we used for producing the experimental data is implemented as a prototype in the open source model checking framework <a href="http://theta.inf.mit.bme.hu">Theta</a>. Source code is available on <a href="https://github.com/FTSRG/theta">GitHub</a>. The experimental data is based on <a href="https://github.com/FTSRG/theta/tree/be86f967998b7065cd55cb629322bffd8333af54">this commit</a>.</p>
<p><strong>Prerequisites</strong></p>
<p><a href="https://www.oracle.com/technetwork/java/javase/downloads/jdk11-downloads-5066655.html">Java SE Runtime Environment 11</a></p>
<p><strong>Building the tool</strong></p>
<p>See the <a href="http://github.com/ftsrg/theta/blob/be86f967998b7065cd55cb629322bffd8333af54/hu.bme.mit.theta.xta/README.md">build instructions</a>.</p>
<p><strong>Usage</strong></p>
<pre><code>
$ java -jar theta-xta-cli.jar
--clock <LU|FWITP|BWITP> Refinement strategy for clock variables
--discrete <NONE|FWITP|BWITP> Refinement strategy for clock variables
--model <MODEL> Path of the input model
--search <BFS|DFS|RANDOM> Search strategy
</code>
</pre>
<p><strong>Example</strong></p>
<pre><code>
$ java -jar theta-xta-cli.jar --model models\c1.xta --clock FWITP --discrete BWITP --search DFS
</code>
</pre>
<p><strong>Sample output</strong></p>
<pre><code>
AlgorithmTimeInMs: 3482 // Total execution time in ms
ExpandTimeInMs: 2128 // Time spend with expansion in ms
CloseTimeInMs: 1301 // Time spent with covering nodes in ms
ExpandExplRefinementTimeInMs: 901 // Expand refinement time for explicit domain in ms
ExpandZoneRefinementTimeInMs: 84 // Expand refinement time for zone domain in ms
CloseExplRefinementTimeInMs: 890 // Close refinement time for explicit domain in ms
CloseZoneRefinementTimeInMs: 145 // Close refinement time for zone domain in ms
CoverageChecks: 628201 // Number of coverage checks
CoverageAttempts: 6069 // Number of attempts for forced coverage
CoverageSuccesses: 6065 // Number of successes for forced coverage
ExplRefinementSteps: 33560 // Number of refinements steps for explicit domain
ZoneRefinementSteps: 1544 // Number of refinements steps for zone domain
ArgDepth: 879 // Depth of the reachability graph
ArgNodes: 14973 // Number of nodes in the reachability graph
ArgNodesExpanded: 9307 // Number of expanded nodes in the reachability graph
</code>
</pre>
<p>For the experiments, we used JVM switches <code>-Xmx6G</code> and <code>-Xss8m</code>.</p>
https://doi.org/10.5281/zenodo.3965792
oai:zenodo.org:3965792
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3965791
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Supplementary Material for the Paper "Configurable Verification of Timed Automata with Discrete Variables"
info:eu-repo/semantics/other
oai:zenodo.org:1308969
2020-01-25T07:23:29Z
software
user-ftsrg
Kristóf, Marussy
Oszkár, Semeráth
Dániel, Varró
2018-07-10
<p><em>ViewModel</em> is a view transformation approach with (1) a fully compositional transformation language built on top of the VIATRA Query language, and (2) a transformation engine which is reactive, incremental, validating and inconsistency-tolerant at the same time.</p>
<p>This deposit contains a snapshot of the source code repository, pre-packaged Eclipse update sites and Eclipse products, as well as reports and raw data for the benchmarks used in our paper: Kristóf Marussy, Oszkár Semeráth and Dániel Varró. "Incremental View Model Synchronization Using Partial Models".</p>
<p>See the enclosed file <strong>README.md</strong> for more information.</p>
https://doi.org/10.5281/zenodo.1308969
oai:zenodo.org:1308969
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1308968
info:eu-repo/semantics/openAccess
Eclipse Public License 1.0
http://www.eclipse.org/legal/epl-v10.html
MODELS, ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems, Copenhagen, Denmark, 14-19 October 2018
view model
model transformation
partial model
ViewModel Tool and Benchmark Results for "Incremental View Model Synchronization Using Partial Models"
info:eu-repo/semantics/other
oai:zenodo.org:3950552
2020-07-30T13:20:21Z
software
user-ftsrg
Oszkár Semeráth
Aren Babikian
Anqi Li
Kristóf Marussy
Dániel Varró
2020-07-17
<p>This deposit contains a virtual machine image for the paper "Automated Generation of Consistent Models with Structural and Attribute Constraints".</p>
<p>The image can be imported into a virtualization environment using the standard <em>.ova</em> format. We recommend using VirtualBox 6.1.10 or later.</p>
<p>For optimum performance, you should increase the memory size and number of CPU cores of the virtual machine to as large as feasible before starting it.</p>
<p>When running the image, you may log in with the <em>models</em> user using the password <em>models20</em>.</p>
<p>Further instructions are provided in the <em>README.md</em> file in the home folder. Select <em>Places > Home</em> from the top bar menu and double-click <em>README.md</em> to access them.</p>
<p>All code of the <a href="https://github.com/viatra/VIATRA-Generator">VIATRA-Generator</a> project is available under the <a href="http://www.eclipse.org/legal/epl-v10.html">Eclipse Public License v1.0</a>. This virtual machine also contains open-source code from other projects, which are available under their respective licenses.</p>
https://doi.org/10.5281/zenodo.3950552
oai:zenodo.org:3950552
Zenodo
https://doi.org/10.1145/3365438.3410962
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3950551
info:eu-repo/semantics/openAccess
Eclipse Public License 1.0
http://www.eclipse.org/legal/epl-v10.html
MODELS, ACM / IEEE 23rd International Conference on Model Driven Engineering Languages and Systems, Sun 18 - Fri 23 October 2020
Artifacts for "Automated Generation of Consistent Models with Structural and Attribute Constraints"
info:eu-repo/semantics/other
oai:zenodo.org:3817874
2020-05-13T20:20:41Z
openaire_data
user-ftsrg
Honfi, Dávid
Micskei, Zoltán
2020-05-08
<p>This package contains the artifacts for our external, differentiated replication of an empirical study on using white-box test generation.</p>
<p>The original experiment is described in the following paper.</p>
<blockquote>
<p>José Miguel Rojas, Gordon Fraser, and Andrea Arcuri. 2015. Automated unit test generation during software development: a controlled experiment and think-aloud observations. In Proceedings of the 2015 International Symposium on Software Testing and Analysis (ISSTA 2015), 338–349. DOI: 10.1145/2771783.2771801</p>
</blockquote>
<p>30 developers and students participated in the experiment in January 2016.</p>
<p>The main difference in the replication was using the IntelliTest test generator tool instead of EvoSuite.</p>
<p>The contents of the package are the followings.</p>
<ul>
<li>/assignments
<ul>
<li>session_starts_endings.csv - Timestamps when each session was started</li>
<li>assignments_with_projects.csv - Assigments of participants to projects, classes and sessions</li>
</ul>
</li>
<li>/projects
<ul>
<li>/golden - Contains the golden implementation and test suites of all 4 classes</li>
<li>/user - Contains the user implementation and test method stubs of all 4 classs</li>
</ul>
</li>
<li>/results
<ul>
<li>time_merged.csv - File of timing analysis containing each test run of subjects</li>
<li>results.csv - Contains the coverage and other required data of each participant tasks</li>
<li>exit.csv - Answers of the exit survey</li>
<li>background.csv - Answers of the background questionnaire</li>
</ul>
</li>
<li>/scripts
<ul>
<li>/ps
<ul>
<li>Get-Results.ps1 - Gets the results of both tasks for one specified participant (invokes MSBuild, MSTest, VisualMutator, OpenCover)</li>
<li>Get-Failures-Errors.ps1 - Gets failures and errors of both tasks for one specified participant (invokes MSBuild, MSTest)</li>
<li>Get-TimeData.ps1 - Iterates over all test runs for each participant</li>
</ul>
</li>
<li>/r
<ul>
<li>likert.R - Generates the Likert chart</li>
<li>si_st.R - Generates table of subject implementation executed with subject test suites</li>
<li>gi_st.R - Generates table of results where subject test suites was run on golden implementation</li>
<li>time_spent_tests.R - Generates a table of time and activity of testing</li>
<li>errors_failures.R - Generates table of errors and failures obtained using the golden test suite</li>
<li>correlation_analysis.R - Generates table containing correlation between lack of correctness and IntelliTest usage</li>
</ul>
</li>
</ul>
</li>
</ul>
https://doi.org/10.5281/zenodo.3817874
oai:zenodo.org:3817874
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3817873
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Using White-Box Test Generation During Development: A Replicated Study
info:eu-repo/semantics/other
oai:zenodo.org:2596044
2020-01-24T19:26:01Z
openaire_data
user-ftsrg
Honfi, David
Micskei, Zoltan
2018-10-27
<p>The data and analysis scripts for our paper entitled Classifying Generated White-Box Tests: An Exploratory Study</p>
https://doi.org/10.5281/zenodo.2596044
oai:zenodo.org:2596044
Zenodo
https://doi.org/10.1007/s11219-019-09446-5
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1472714
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Software Quality Journal, (2018-10-27)
Classifying Generated White-Box Tests: An Exploratory Study
info:eu-repo/semantics/other
oai:zenodo.org:8002253
2023-06-04T02:26:55Z
openaire_data
user-ftsrg
Ádám, Zsófia
Micskei, Zoltán
2023-06-03
<p>Dataset used in the evaluation of Part II of the MSc thesis titled "Extending the Capabilities of the CEGAR Model Checking Algorithm"</p>
https://doi.org/10.5281/zenodo.8002253
oai:zenodo.org:8002253
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.8002252
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Runtime Monitoring of Refinement Progress in CEGAR-based Model Checking: Dataset
info:eu-repo/semantics/other
oai:zenodo.org:3690194
2020-03-01T14:16:23Z
user-ftsrg
Majzik, István
Molnár, Vince
2019-10-30
<p>Formal verification is a collective name of techniques that aim to <em>prove</em> that a system design or implementation satisfies its required properties. Formally proving something is much more challenging than testing and simulation: the proof has to cover every possible case, not just selected executions of the system. This kind of rigorous analysis is often used in the development of safety-critical hardware and software systems, commonly found in the automotive, railway or aerospace industries.</p>
<p>Model checking is an automated formal verification technique that evaluates the possible states and behaviors of a system design with regard to a formal specification. This is a challenging task because real-life systems usually have an enormous number of possible states, all (or most) of which has to be checked for violations of the specified properties. Symbolic model checking techniques, and in particular the saturation algorithm have been introduced to efficiently handle these large state spaces in many (common) cases.</p>
<p>Research of the saturation algorithm has yielded different variants suitable for different problems, but the range of possible applications are still not fully covered. This dissertation presents further results in the fields of efficient analysis of models with prioritized transitions and the model checking of linear temporal logic properties, a class of specification logic that is prevalent but hard to analyze. Furthermore, investigation of different variants of saturation inspired an enhanced and more general version of the original algorithm, which is the culmination of this research.</p>
<p>Thesis 1 presents an approach to efficiently analyze Generalized Stochastic Petri Nets, a formalism suitable for the modeling of extra-functional aspects of a system. These models have prioritized transitions, which is challenging for saturation. The presented approach decomposes the priority-related aspects from the effect of the transition and achieves better scaling compared to previous approaches, expanding the scope of models on which analysis is feasible.</p>
<p>Thesis 2 is about the model checking of linear temporal logic properties, which is a complex algorithm only partially supported by saturation. It investigates how saturation can be used in different phases of the algorithm and introduce extensions accordingly. Furthermore, Thesis 2 introduces new algorithms for the different subtasks of this model checking problem, tailored to work with saturation and combining the best of previously known approaches. The combination of these building blocks provides a scalable, optimized symbolic model checking algorithm for linear temporal logic properties.</p>
<p>Thesis 3 introduces an enhanced version of the saturation algorithm. By identifying the common ideas, the enhanced version generalizes previous variants in a single, more powerful algorithm that can directly tackle a wider range of problems. Enhancement can be observed on performance as well: in certain types of models, the enhanced version outperforms the original saturation algorithm by orders of magnitude, while it has the same performance in other cases.</p>
Successfully defended on February 18, 2020.
https://doi.org/10.5281/zenodo.3690194
oai:zenodo.org:3690194
eng
Zenodo
https://hdl.handle.net/10890/13340
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3690193
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
formal verification
model checking
saturation
decision diagram
Petri net
priority
linear temporal logic
generalized Saturation
conditional locality
Extensions and Generalization of the Saturation Algorithm in Model Checking
info:eu-repo/semantics/doctoralThesis
oai:zenodo.org:6889008
2022-08-11T00:09:35Z
software
user-ftsrg
Földiák, Máté
Marussy, Kristóf
Varró, Dániel
Majzik, István
2022-07-23
<p>Our paper proposes two logic solver-based approaches to evaluate complex design spaces by using partial models in order to find an optimal solution with respect to performability objectives. One approach uses performability analysis as a post-filtering of valid system architecture candidates, while the other approach uses performability analysis for guiding the actual search over partial models. Our approaches are implemented in a prototype tool based on the VIATRA-Solver framework and using the PRISM Stochastic Model Checker for performability analysis. We evaluate both approaches on an interferometry mission architecture case study using view transformations for performability analysis and compare our approach with the well-known MOMoT framework based on meta-heuristic search. The artifact contains source code, a Docker image for running the experiments, and a virtual machine for data analysis.</p>
https://doi.org/10.5281/zenodo.6889008
oai:zenodo.org:6889008
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.6889007
info:eu-repo/semantics/openAccess
Eclipse Public License 1.0
http://www.eclipse.org/legal/epl-v10.html
performability
design-space exploration
logic solver
model generator
partial models
Artifacts for "System Architecture Synthesis for Performability by Logic Solvers"
info:eu-repo/semantics/other
oai:zenodo.org:4483627
2021-02-01T00:27:18Z
software
user-ftsrg
Ádám, Zsófia
Sallai, Gyula
Hajdu, Ákos
2021-01-31
<p>This archive contains Gazer v1.2.1 and Theta v2.5.0, which were used in <a href="https://sv-comp.sosy-lab.org/2021/">SV-COMP 2021</a>. Also available at the <a href="https://gitlab.com/sosy-lab/sv-comp/archives-2021/-/tree/svcomp21/2021">SV-COMP 2021 repository</a>.</p>
https://doi.org/10.5281/zenodo.4483627
oai:zenodo.org:4483627
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.4483626
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Gazer
Theta
SV-COMP
Software verification
Gazer-Theta SV-COMP 2021 Competition Contribution
info:eu-repo/semantics/other
oai:zenodo.org:4665613
2021-04-07T00:27:25Z
user-ftsrg
Marussy, Kristóf
Dániel, Szekeres
2021-04-06
<p>The failure of complex safety-critical cyber-physical systems can endanger human lives, or cause a high amount of financial loss. Throughout the development of such systems, taking extra-functional requirements - like safety, reliability and performance - into account is of utmost importance. These kinds of requirements are mostly quantitative, meaning that they give target values for some metrics of the system that must be achieved. Achieving these values must be assured already in the design phase, when no usable instance of the system under development is available for measurement, only a model describing its behavior.</p>
<p>The reliability and availability metrics are derived using a stochastic model explicitly describing the randomness inherent in the behavior of the system. In my work, I focus on a widely used stochastic modeling formalism called fault trees. This formalism is based on the decomposition of the system-level error: it describes the system-level error as a logic function of the error of the system's elementary components.</p>
<p>To calculate the necessary metrics from the model, like mean time to first failure, a lower level analysis model must be derived from it, that can be handled mathematically. When creating and analyzing this low-level model, the problem of state-space explosion arises: even though the high-level engineering model is of tractable size, the size of the corresponding analysis model is exponential in the original one's size. Because of this, the scalability of widespread explicit analysis methods is limited.</p>
<p>A possible solution to this problem is storing the linear equation system that needs to be solved during the analysis in a concise approximate form using tensor representation methods, and seeking the solution in the same format. I examined the applicability of Tensor Train (TT) methods for fault tree in my work. I use decision diagram-based state space representation for the derivation of the compressed form, which is widely used in symbolic model checking.</p>
<p>There are several different iterative algorithms for solving equation systems in the TT format to perform the necessary calculations. Throughout my work I compare and extend these methods for the solution of problems arising in the analysis of fault trees.</p>
<p>I verify the correctness of the theoretical results through measurements performed on large fault trees, using not just the iterative TT algorithm, but widely used explicit methods as well.</p>
https://doi.org/10.5281/zenodo.4665613
oai:zenodo.org:4665613
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.4665612
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Towards tensor-based reliability analysisof complex safety-critical systems
info:eu-repo/semantics/doctoralThesis
oai:zenodo.org:7455304
2022-12-19T02:26:48Z
software
user-ftsrg
Bajczi, Levente
Telbisz, Csanád
Somorjai, Márk
Dobos-Kovács, Mihály
Ádám, Zsófia
Molnár, Vince
2022-12-18
<p>This archive contains the tool archive of Theta for SV-COMP 2023, which was also added as a release to the tool (<a href="https://github.com/ftsrg/theta/releases/tag/svcomp23">here</a>).</p>
https://doi.org/10.5281/zenodo.7455304
oai:zenodo.org:7455304
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.7455303
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
CEGAR-based Verification of Concurrent and Recursive Programs in Theta (Competition Contribution): Tool Archive
info:eu-repo/semantics/other
oai:zenodo.org:3402868
2020-06-15T09:21:10Z
openaire_data
user-ftsrg
Hajdu, Ákos
Micskei, Zoltán
2019-09-09
<p>Supplementary material for the paper "Efficient Strategies for CEGAR-based Model Checking" by Akos Hajdu and Zoltan Micskei. The material includes a detailed report (report.html) and all artifacts to replicate our measurements and analysis (artifact.tar.gz).</p>
<p><em>This is the version that corresponds to the final, published paper.</em></p>
https://doi.org/10.5281/zenodo.3402868
oai:zenodo.org:3402868
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1252784
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Formal verification
Abstraction
CEGAR
Experimental evaluation
Supplementary Material for the paper "Efficient Strategies for CEGAR-based Model Checking"
info:eu-repo/semantics/other
oai:zenodo.org:1117854
2020-01-24T19:25:32Z
openaire_data
user-ftsrg
Ákos Hajdu
Zoltán Micskei
2017-12-18
<p> A supplementary report for the paper "A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework" by Ákos Hajdu and Zoltán Micskei, presented at the 25th PhD Mini-Symposium (2018), organized by the Department of Measurement and Information Systems at the Budapest University of Technology and Economics.</p>
https://doi.org/10.5281/zenodo.1117854
oai:zenodo.org:1117854
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1117853
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
25th PhD Mini-Symposium, Budapest, Hungary, 29-30 January 2018
formal verification
cegar
theta
randomization
experimental evaluation
Supplementary Report for the paper "A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework"
info:eu-repo/semantics/other
oai:zenodo.org:1158043
2020-01-24T19:25:22Z
openaire_data
user-ftsrg
Ákos Hajdu
Zoltán Micskei
2018-01-29
<p> A supplementary report for the paper "A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework" by Ákos Hajdu and Zoltán Micskei, presented at the 25th PhD Mini-Symposium (2018), organized by the Department of Measurement and Information Systems at the Budapest University of Technology and Economics.</p>
https://doi.org/10.5281/zenodo.1158043
oai:zenodo.org:1158043
eng
Zenodo
https://doi.org/10.5281/zenodo.1219261
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1117853
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
25th PhD Mini-Symposium, Budapest, Hungary, 29 January 2018
formal verification
cegar
theta
randomization
experimental evaluation
abstraction
Supplementary Report for the paper "A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework"
info:eu-repo/semantics/other
oai:zenodo.org:1318156
2020-01-25T07:23:30Z
software
user-ftsrg
Kristóf, Marussy
Oszkár, Semeráth
Dániel, Varró
2018-07-20
<p><em>ViewModel</em> is a view transformation approach with (1) a fully compositional transformation language built on top of the VIATRA Query language, and (2) a transformation engine which is reactive, incremental, validating and inconsistency-tolerant at the same time.</p>
<p>This deposit contains a snapshot of the source code repository, pre-packaged Eclipse update sites and Eclipse products, as well as reports and raw data for the benchmarks used in our paper: <a href="https://doi.org/10.1145/3239372.3239412">Kristóf Marussy, Oszkár Semeráth </a><a href="https://doi.org/10.1145/3239372.3239412">and</a><a href="https://doi.org/10.1145/3239372.3239412"> Dániel Varró. "Incremental View Model Synchronization Using Partial Models"</a>.</p>
<p>See the enclosed file <strong>README.md</strong> for more information.</p>
<p><a href="https://github.com/modelsconf2018/artifact-evaluation/issues/14#issuecomment-406573285">Approved</a> by the <a href="https://modelsconf2018.github.io/calls/artifact-evaluation/">MODELS '18 Artifact Evaluation Committee</a>.</p>
https://doi.org/10.5281/zenodo.1318156
oai:zenodo.org:1318156
eng
Zenodo
https://doi.org/10.1145/3239372.3239412
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1308968
info:eu-repo/semantics/openAccess
Eclipse Public License 1.0
http://www.eclipse.org/legal/epl-v10.html
MODELS, ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems, Copenhagen, Denmark, 14-19 October 2018
view model
model transformation
partial model
ViewModel Tool and Benchmark Results for "Incremental View Model Synchronization Using Partial Models"
info:eu-repo/semantics/other
oai:zenodo.org:2597969
2020-01-20T17:02:46Z
user-ftsrg
Bajkai, Viktória Dorina
Hajdu, Ákos
2019-01-24
<p>Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.</p>
https://doi.org/10.5281/zenodo.2597969
oai:zenodo.org:2597969
eng
Budapest University of Technology and Economics, Department of Measurement and Information Systems
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.2597968
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
26th PhD Mini-Symposium, Budapest, Hungary, 24 January 2019
verification
abstraction
CEGAR
Software Model Checking with a Combination of Explicit Values and Predicates
info:eu-repo/semantics/conferencePaper
oai:zenodo.org:3892347
2020-12-02T12:27:16Z
user-ftsrg
Micskei, Zoltán
Hajdu, Ákos
2020-06-14
<p>Formal verification techniques allow rigorous reasoning about the operation of computer systems and programs. With a sound and complete mathematical basis, it is both possible to show the presence of certain kinds of errors and to prove their absence. Formal methods are often applied in critical domains (e.g., industrial controllers) to increase quality and trust in their correct operation. However, most of the interesting questions to be analyzed are computationally complex or undecidable in general. Therefore, verification approaches in different problem domains usually put more emphasis on different properties of the analysis to achieve a reasonable trade-off. Such properties include (1) expressive power (2) efficiency, and (3) the amount of conclusive answers. This work addresses challenges related to the properties mentioned above in three different problem domains using different approaches to make verification effective.</p>
<p>Thesis 1 targets concurrent and asynchronous systems by modeling them with Petri nets and checking the reachability of a given state. We study an existing algorithm that uses an efficient structural over-approximation. However, the expressive power is limited to simple reachability properties and the algorithm can easily give inconclusive answers due to its iteration strategy. We lift the expressive power of the algorithm by handling a generalized version of reachability and supporting Petri nets extended with inhibitor arcs. We increase the number of conclusive answers by the algorithm via a new iteration approach on invariants and a hybrid search strategy.</p>
<p>Thesis 2 targets embedded software code by modeling them with control-flow automata and checking the reachability of a distinguished error location. We study abstraction-refinement-based model checking where efficiency is still a significant limitation due to the complexity of the programs and the rich domains of their variables. We propose various efficient strategies for both abstraction and refinement. For abstraction, we extend the explicit-value analysis with limited successor enumeration, and we adapt structural information from the program to guide the search more efficiently. For refinement, we develop a backward-search based interpolation strategy and an approach that uses multiple counterexamples for a faster convergence to the appropriate level of abstraction.</p>
<p>Thesis 3 targets decentralized, blockchain-based systems by translating contracts (programs running on such systems) to an intermediate verification language.<br>
We adapt existing modular specification constructs to this context and also propose domain-specific properties. This provides a flexible and expressive approach to specify high-level, functional properties of contracts. We define a translation from contracts to the Boogie intermediate verification language, and leverage existing modular verification approaches. Furthermore, we develop a modular encoding of arithmetic that can capture operations precisely and efficiently over large bit-widths that are common in this domain.</p>
<p>All contributions have been implemented in practical tools and are available publicly. We also evaluate our contributions on various synthetic and real-world examples to prove their applicability. Results show that our contributions successfully address the targeted challenges and provide effective verification approaches in general.</p>
Public defense: 24 November 2020. Reviewers: Prof. Florian Zuleger and Dr. Ákos Kiss.
https://doi.org/10.5281/zenodo.3892347
oai:zenodo.org:3892347
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3892346
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Effective Domain-Specific Formal Verification Techniques
info:eu-repo/semantics/doctoralThesis
oai:zenodo.org:1477670
2020-01-24T19:25:54Z
openaire_data
user-ftsrg
Honfi, David
Micskei, Zoltan
2018-10-27
<p>The data and analysis scripts for our paper entitled Classifying Generated White-Box Tests: An Exploratory Study</p>
https://doi.org/10.5281/zenodo.1477670
oai:zenodo.org:1477670
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1472714
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Classifying Generated White-Box Tests: An Exploratory Study
info:eu-repo/semantics/other
oai:zenodo.org:7922895
2023-05-11T14:26:43Z
user-ftsrg
Horváth, Benedek
Molnár, Vince
Graics, Bence
Hajdu, Ákos
Ráth, István
Horváth, Ákos
Karban, Robert
Trancho, Gelys
Micskei, Zoltán
2023-01-24
<p>This report is supplementary material to the paper Horváth et al. <em>Pragmatic Verification and Validation of Industrial Executable SysML Models</em>. It provides insights into the transformation rules between SysML and Gamma, both on the conceptual and the technical<br>
level.</p>
https://doi.org/10.5281/zenodo.7922895
oai:zenodo.org:7922895
Zenodo
https://doi.org/10.1002/sys.21679
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.7564294
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
formal verification, model-based systems engineering, model transformation, model checking
Supplementary Material to the Pragmatic Verification and Validation of Industrial Executable SysML Models
info:eu-repo/semantics/technicalDocumentation
oai:zenodo.org:4267044
2020-11-10T22:44:12Z
user-ftsrg
Micskei, Zoltán
Honfi, Dávid
2020-11-10
<p>Software testing is an inevitable part of software development to ensure the quality of the product. Thorough testing of software, however, might consume an significant amount of time and resources. Therefore, already decades ago, research has begun to reduce this effort by automating the process, while improving the efficiency of testing as well. One of the recommended methods is white-box test generation, which uses only the source code to generate test cases. Although there are several types of techniques using this idea - including symbolic execution, search-based testing, and guided random testing - the complexity of real-world software can make their application burdensome. These techniques usually suffer from issues, when the software under test interacts with its environment, structured objects should be created for good coverage, valid test oracles should be guessed, or the size of the program is too large. Furthermore, the use of such advanced techniques is not trivial for ordinary developers or testers due to their underlying complexity, hence the identification of test generation problems can be a difficult task as well. This work empirically evaluates these challenges and addresses some of them by proposing new techniques and tools for white-box test generation.</p>
https://doi.org/10.5281/zenodo.4267044
oai:zenodo.org:4267044
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.4266975
info:eu-repo/semantics/restrictedAccess
software testing
test generation
white-box testing
symbolic execution
empirical study
Evaluating and Improving White-Box Test Generation
info:eu-repo/semantics/doctoralThesis
oai:zenodo.org:8188658
2023-07-27T15:48:52Z
openaire_data
user-ftsrg
Elekes, Márton
Molnár, Vince
Micskei, Zoltán
2023-07-27
<p>This dataset provides artifacts about the semantics of doActivity in the Precise Semantics of UML State Machines (PSSM) specification. It collects execution traces and screenshots from two simulators (Cameo, Papyrus Moka), and analysis about doActivity features present in PSSM test suite, focusing on concurrency.</p>
https://doi.org/10.5281/zenodo.8188658
oai:zenodo.org:8188658
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.8188657
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
UML
state machine
semantics
Supplementary Material for "To Do or Not to Do: Semantics and Patterns for Do Activities in UML PSSM State Machines"
info:eu-repo/semantics/other
oai:zenodo.org:1219234
2020-01-20T14:28:29Z
user-ftsrg
Dávid Honfi
Zoltán Micskei
2018-01-29
<p>Conference paper appeared in the Proceedings of the 25th PhD Mini-Symposium at the Department of Measurement and Information Systems, Budapest University of Technology and Economics.</p>
https://doi.org/10.5281/zenodo.1219234
oai:zenodo.org:1219234
Zenodo
isbn:978-963-313-285-2
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1219233
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Towards Supporting Dynamic Symbolic Execution via Multi-Domain Metrics
info:eu-repo/semantics/conferencePaper
oai:zenodo.org:4110043
2020-10-21T00:26:56Z
user-ftsrg
Mondok, Milán
Vörös, András
2020-02-05
<p>Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of "lasso"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.</p>
https://doi.org/10.5281/zenodo.4110043
oai:zenodo.org:4110043
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.4110042
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
MINISY@DMIS 2020, 27th Minisymposium of the Department of Measurement and Information Systems, Budapest, 05-06 February 2020
cegar
ltl
model checking
formal verification
temporal logic
Abstraction-Based Model Checking of Linear Temporal Properties
info:eu-repo/semantics/conferencePaper
oai:zenodo.org:3668974
2020-02-17T07:20:56Z
openaire_data
user-ftsrg
David Honfi
Zoltan Micskei
2019-09-22
<p>We present an approach for automated isolation in white-box test generation. This publication contains the data and the corresponding analysis script written in R.</p>
https://doi.org/10.5281/zenodo.3668974
oai:zenodo.org:3668974
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.3457479
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
testing
test generation
white-box
isolation
Automated Isolation for White-box Test Generation
info:eu-repo/semantics/other
oai:zenodo.org:5956737
2022-02-03T13:49:38Z
openaire_data
user-ftsrg
Zsófia Ádám
Levente Bajczi
Mihály Dobos-Kovács
Ákos Hajdu
Vince Molnár
2022-02-02
<p>This archive contains the tool archive of Theta for SV-COMP 2022, which was also added as a release to the tool (<a href="https://github.com/ftsrg/theta/releases/tag/svcomp22-v1">here</a>).</p>
https://doi.org/10.5281/zenodo.5956737
oai:zenodo.org:5956737
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.5956736
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution): Tool Archive
info:eu-repo/semantics/other
oai:zenodo.org:6974248
2022-08-11T02:26:30Z
software
user-ftsrg
Földiák, Máté
Marussy, Kristóf
Varró, Dániel
Majzik, István
2022-07-23
<p>Our paper proposes two logic solver-based approaches to evaluate complex design spaces by using partial models in order to find an optimal solution with respect to performability objectives. One approach uses performability analysis as a post-filtering of valid system architecture candidates, while the other approach uses performability analysis for guiding the actual search over partial models. Our approaches are implemented in a prototype tool based on the VIATRA-Solver framework and using the PRISM Stochastic Model Checker for performability analysis. We evaluate both approaches on an interferometry mission architecture case study using view transformations for performability analysis and compare our approach with the well-known MOMoT framework based on meta-heuristic search. The artifact contains source code, a Docker image for running the experiments, and a virtual machine for data analysis.</p>
https://doi.org/10.5281/zenodo.6974248
oai:zenodo.org:6974248
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.6889007
info:eu-repo/semantics/openAccess
Eclipse Public License 1.0
http://www.eclipse.org/legal/epl-v10.html
performability
design-space exploration
logic solver
model generator
partial models
Artifacts for "System Architecture Synthesis for Performability by Logic Solvers"
info:eu-repo/semantics/other
oai:zenodo.org:2704320
2020-01-20T15:57:02Z
user-ftsrg
Szanto, Tamas
Micskei, Zoltan
2019-01-24
<p>Machine Learning (ML) techniques, especially Deep Neural Networks are achieving compelling results in many fields. However, the integration of ML solutions into critical systems where trustworthiness, reliability, and safety are crucial is an unsolved problem. The datasets have great importance for Machine Learning algorithms since the achievable precision during the training, and the accuracy of the final evaluation rely both on the quality and quantity of the data. Our goal was to improve the measurement of the quality of datasets. We recommend to 1) use the requirements gathered during systems design, and 2) generate metrics, which can provide information about the representativeness of a dataset to determine which are the problems that we can safely solve by using the data. This paper describes a general method for dataset evaluation using multiple measurement techniques, including prediction explanations. The method is demonstrated by applying it to a case study of categorising road signs.</p>
https://doi.org/10.5281/zenodo.2704320
oai:zenodo.org:2704320
Budapest University of Technology and Economics, Department of Measurement and Information Systems
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.2704319
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
26th PhD Mini-Symposium, Budapest, Hungary, 24 January 2019
testing
machine learning
dataset
V&V
Measuring quality of datasets using prediction explanation
info:eu-repo/semantics/conferencePaper
oai:zenodo.org:804002
2020-01-24T19:22:50Z
openaire_data
user-ftsrg
Honfi, Dávid
Micskei, Zoltán
2017-06-07
<p>White-box test generator tools rely only on the code under test to select test inputs, and capture the implementation's output as assertions. If there is a fault in the implementation, it could get encoded in the generated tests. Tool evaluations usually measure fault-detection capability using the number of such fault-encoding tests. However, these faults are only detected, if the developer can recognize that the encoded behavior is faulty. We designed an exploratory study to investigate how developers perform in classifying generated white-box test as faulty or correct. We carried out the study in a laboratory setting with 54 graduate students. The tests were generated for two open-source projects with the help of the IntelliTest tool. The performance of the participants were analyzed using binary classification metrics and by coding their observed activities. The results showed that participants incorrectly classified a large number of both fault-encoding and correct tests (with median misclassification rate 33% and 25% respectively). Thus the real fault-detection capability of test generators could be much lower than typically reported, and we suggest to take this human factor into account when evaluating generated white-box tests.<br>
<br>
This material contains the dataset and the recorded videos of the study.</p>
https://doi.org/10.5281/zenodo.804002
oai:zenodo.org:804002
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.804001
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
software testing
test generation
white-box testing
empirical study
Classifying the Correctness of Generated White-Box Tests: An Exploratory Study
info:eu-repo/semantics/other
oai:zenodo.org:2571853
2020-06-15T09:21:10Z
openaire_data
user-ftsrg
Hajdu, Ákos
Micskei, Zoltán
2019-02-18
<p>Supplementary material for the paper "Efficient Strategies for CEGAR-based Model Checking" by Akos Hajdu and Zoltan Micskei. The material includes a detailed report (report.html) and all artifacts to replicate our measurements and analysis (artifact.tar.gz).</p>
https://doi.org/10.5281/zenodo.2571853
oai:zenodo.org:2571853
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1252784
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Formal verification
Abstraction
CEGAR
Experimental evaluation
Supplementary Material for the paper "Efficient Strategies for CEGAR-based Model Checking"
info:eu-repo/semantics/other
oai:zenodo.org:1252785
2020-06-15T09:21:09Z
openaire_data
user-ftsrg
Hajdu, Ákos
Micskei, Zoltán
2018-05-25
<p>A supplementary report for the paper "Efficient Strategies for CEGAR-based Model Checking" by Akos Hajdu and Zoltan Micskei, including the raw data, the R script and a detailed report (in pdf and html formats).</p>
https://doi.org/10.5281/zenodo.1252785
oai:zenodo.org:1252785
eng
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1252784
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Formal verification
Abstraction
CEGAR
Experimental evaluation
Supplementary Report for the paper "Efficient Strategies for CEGAR-based Model Checking"
info:eu-repo/semantics/other
oai:zenodo.org:2596041
2020-01-24T19:25:54Z
openaire_data
user-ftsrg
Honfi, David
Micskei, Zoltan
2018-10-27
<p>The data and analysis scripts for our paper entitled Classifying Generated White-Box Tests: An Exploratory Study</p>
https://doi.org/10.5281/zenodo.2596041
oai:zenodo.org:2596041
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1472714
info:eu-repo/semantics/openAccess
Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
Classifying Generated White-Box Tests: An Exploratory Study
info:eu-repo/semantics/other
oai:zenodo.org:1472715
2020-01-24T19:25:53Z
openaire_data
user-ftsrg
Honfi, David
Micskei, Zoltan
2018-10-27
<p>The data and analysis scripts for our paper entitled Classifying Generated White-Box Tests: An Exploratory Study</p>
https://doi.org/10.5281/zenodo.1472715
oai:zenodo.org:1472715
Zenodo
https://zenodo.org/communities/ftsrg
https://doi.org/10.5281/zenodo.1472714
info:eu-repo/semantics/restrictedAccess
Classifying Generated White-Box Tests: An Exploratory Study
info:eu-repo/semantics/other