Peleska, Jan
Lade...
Preferred name
Peleska, Jan
Official Name
Peleska, Jan
ORCID
GND
5 Ergebnisse
Einstellungen
Gerade angezeigt 1 - 5 von 5
- Some of the metrics are blocked by yourconsent settings
Item-typ:Veröffentlichung, Automatisierte Testdatengenerierung hybrider diskret-kontinuierlicher eingebetteter Systeme(2010-06-28); ; ; In this dissertation we present an incremental approach to solve the Satisfiability (SAT) Problem for the automated test case generation of hybrid discrete and continuous embedded systems using background theory solvers of the linear arithmetic (LA) and fixed-size bit-vectors (BV) for quantifier-free first-order formulae. Both of these theory solvers extend the Davis-Putnam-Logemann-Loveland decision procedure (DPLL), which was initially designed to solve the satisfiability problem in the propositional logic, to the first-order logic. Furthermore the both theory solvers can be integrated in a lazy SMT-Theorem Prover - also known as Satisfiability Modulo Theory - as a decision procedure for the conjunction of literals in their specified theories and implement theory-driven deduction, learning and backjumping techniques to enhance the efficiency of the SMT-Theorem Prover.Dissertation312 165 - Some of the metrics are blocked by yourconsent settings
Item-typ:Veröffentlichung, Executable HybridUML Semantics.A Transformation Definition.(2005-12-14); ; ; This thesis contributes to the development of hybrid systems. For the particular specification formalism HybridUML, a formally defined transformation Phi of HybridUML models into executable low-level models is defined. The resulting low-level models have a formal semantics, therefore by Phi, this formal semantics is assigned to the corresponding HybridUML models. As a result, there is no inconsistency between the HybridUML specification of a hybrid system and its implementation. HybridUML is derived from the Unified Modeling Language, which is a wide-spread modeling language for the development of software systems. The semantics is executable, i.e. executable code is automatically generated from HybridUML models, such that they are directly usable in practice.Chapter 1 motivates the use of the specification formalism HybridUML for the formal definition of hybrid systems. As an approach to combine the definition of hybrid systems in a formal, but user-friendly way, with the generation of a resulting executable system that has formally defined behavior, a transformation concept is proposed: Hybrid systems models are modeled with the specification language HybridUML, and are transformed into programs of the Hybrid Low-Level Framework HL3, which provides a restricted design pattern that the transformation has to comply with, as well as a runtime environment that provides basic functionality.Chapter 2 defines the HybridUML Mathematical Meta-Model, which is a non-graphical definition of the HybridUML syntax. The separation of the meta-model from its graphical representation is the usual UML approach, and the benefits are that (1) the meta-model is directly usable for transformation Phi, and that (2) the HybridUML semantics is independent from the graphical notation. In chapter 3, the expressions that can be used within a HybridUML model, e.g. boolean expressions from mode invariants or transition conditions, or assignment expressions from transition actions, are defined by means of the HybridUML Expression Language.The HL3 Low-Level Framework is discussed in chapter 4. It is a compilation target for hybrid systems specification formalisms. A formal operational semantics is given for the execution of HL3 models, which are defined as a mixture of explicit program code and abstractions to mathematical representations.The specific transformation Phi_HUML from HybridUML models to instances of the HL3 framework is presented in chapter 5. The transformation is defined formally, therefore the HybridUML executable semantics results.The thesis is concluded in chapter 6. A summary is given, and the main scientific contributions are pointed out. Possible future work related to HybridUML, to the low-level framework HL3, and to the transformational approach is discussed.Dissertation596 193 - Some of the metrics are blocked by yourconsent settings
Item-typ:Veröffentlichung, An approach for the verification and synthesis of complete test generation algorithms for finite state machines(2022-07-20); ; ; Complete test suites are of special interest in the field of model-based testing, as they guarantee high fault detection capabilities under well-specified assumptions. The variety and complexity of strategies generating complete test suites, their implementations, and their completeness proofs impose difficulties upon manual verification. Furthermore, ambiguities or only implicitly specified assumptions in natural language descriptions and proofs easily lead to implementations that do not generate complete test suites. The present dissertation proposes an alternative approach to the verification and implementation of test strategies that generate complete test suites for testing for language-equivalence on finite state machines, that employs the interactive theorem prover Isabelle. In the first part of this work, similarities and differences between steps performed by the considered test strategies are identified. From these, a framework is derived as a higher order function capable of representing all considered strategies as concrete applications of it. Several implementations of parameters of this framework are shared between multiple strategies. Additional frameworks are developed to support alternative completeness proofs. The second part of this work defines finite state machines, their properties and operations, as well as the frameworks in Isabelle/HOL and respectively proves them correct and complete. Completeness proofs over frameworks are decoupled from concrete implementations of their parameters by suitable interfaces. This approach enables the reuse of proofs between similar strategies and thus simplifies completeness proofs for new variations on already handled strategies. Finally, the definitions in Isabelle are employed to automatically generate provably correct implementations of the considered test strategies. It is shown that these exhibit comparable performance to a manually developed C++ library for certain inputs.Dissertation537 445 - Some of the metrics are blocked by yourconsent settings
Item-typ:Veröffentlichung, Complete property-oriented testing(2024-06-18); ; ; This PhD thesis introduces new methods for property-oriented testing of systems with finite internal states but potentially infinite input/output domains. It focuses on properties defined in Linear Temporal Logic (LTL) and uses Symbolic Finite State Machines (SFSMs) for modeling. The thesis addresses gaps in existing literature by providing exhaustive testing approaches. Two main methods are presented: The first is a model-based testing approach that modifies traditional conformance testing for FSMs to work with SFSMs, enabling exhaustive property violation checks with potentially smaller test suites. The second is a complete property-oriented testing approach based on black box checking, which is enhanced to work with SFSMs and optimized for better runtime performance through reduced equivalence checks and the incorporation of fuzzing. Both methods are evaluated for their efficacy through automation and experiments, and further optimizations are discussed.Dissertation117 153 - Some of the metrics are blocked by yourconsent settings
Item-typ:Veröffentlichung, Integrated Module Testing and Module Verification(2013-12-10); ; ; In this dissertation an integrated approach to formal module verification by model checking and module testing is described. The main focus lays on the verification of C functions. Specification-based testing and functional verification require a formalized module specification. For this purpose an annotation language as an extension of a pre-/post-condition syntax is developed and discussed. This annotation language allows the definition of logical conditions relating the program s pre-state to its post-state after executing the module. For requirements tracking a test case specification is developed. The correctness conditions can be refined by the introduction of auxiliary variables. Besides the specification of the module under test, the presented annotation language allows to model the behavior of external functions called by the module under test. By the specification of pre- and post-conditions as well as test cases, test data generation for both structural and functional testing is reduced to a reachability problem (as known from bounded model checking) within the module s control flow graph. These reachability problems are investigated using symbolic execution. The strength of symbolic execution is in its precision and its ability to reason about multiple program inputs simultaneously, but it also has limitations like aliasing or external function calls. These in turn are analyzed and new algorithms are developed which overtake most of the detected limitations. The expansion and selection strategies for test case selection are developed and described. They allow to minimize the size of investigated states and the number of generated test cases, while achieving maximal branch coverage. The developed algorithms and strategies are implemented in the test generator CTGEN, which generates test data for C1 structural coverage and for functional coverage. It also supports automated stub generation where the data returned by a stub during test execution depends on the specification provided by the user. CTGEN is evaluated and compared with competing tools and produces competitive results.Dissertation836 239