@misc{NoackHelkeKarbe, author = {Noack, Thomas and Helke, Steffen and Karbe, Thomas}, title = {Reuse-Based Test Traceability: Automatic Linking of Test Cases and Requirements}, series = {International Journal on Advances in Software}, volume = {7}, journal = {International Journal on Advances in Software}, number = {3-4}, issn = {1942-2628}, pages = {469 -- 485}, abstract = {Safety standards demand full requirement traceability, which includes a complete tracing between requirements and test cases to stipulate how a requirement has to be verified. However,implementing such a concept rigorously is time-consuming and costly. Furthermore, in the automotive industry this cost is repeatedly incurred for each vehicle series, because in contrast to other development artefacts, reuse strategies for trace links have not yet been sufficiently researched. This paper presents the novel approach of Reuse-based Test Traceability, which allows for a more cost-effective implementation of trace links in certain cases. First, we identify and formalize a scenario, the so called RT-Problem, for reusing trace links between test cases and reused requirements, which has been observed in industry practice. Next, based on this formalization we propose a 3-layered method, which automatically creates links between test cases and reused requirements. For reasons of practicality, we focus on the first layer, which represents a transitive test-link reuse. Finally, we present the results of two field studies demonstrating that our approach is feasible in practice. As the main contribution of this work we show that the automated reuse of test cases on the basis of reused requirements is both possible and useful.}, language = {en} } @inproceedings{HelkeKammuellerProbst, author = {Helke, Steffen and Kamm{\"u}ller, Florian and Probst, Christian W.}, title = {Secure Refactoring with Java Information Flow}, series = {Data Privacy Management, and Security Assurance, 10th International Workshop, DPM 2015, and 4th International Workshop, QASA 2015, Vienna, Austria, September 21-22, 2015}, booktitle = {Data Privacy Management, and Security Assurance, 10th International Workshop, DPM 2015, and 4th International Workshop, QASA 2015, Vienna, Austria, September 21-22, 2015}, editor = {Garcia-Alfaro, Joaquin and Navarro-Arribas, Guillermo and Aldini, Alessandro and Martinelli, Fabio and Suri, Neeraj}, publisher = {Springer}, address = {Cham}, isbn = {978-3-319-29882-5}, doi = {10.1007/978-3-319-29883-2}, pages = {264 -- 272}, abstract = {Refactoring means that a program is changed without changing its behaviour from an observer's point of view. Does the change of behaviour also imply that the security of the program is not affected by the changes? Using Myers and Liskov's distributed information flow control model DLM and its Java implementation Jif, we explore this question practically on common patterns of Refactoring as known from Fowler. We first illustrate on an example the "Extract method" refactoring and how it can endanger confidentiality. We then show how to construct a secure version of this major refactoring pattern by employing Jif to control information flows. Finally, we can show that security leaks as encountered at the outset are not possible anymore.}, language = {en} } @misc{HelkeKammueller, author = {Helke, Steffen and Kamm{\"u}ller, Florian}, title = {Verification of Statecharts Using Data Abstraction}, series = {International Journal of Advanced Computer Science and Applications}, volume = {7}, journal = {International Journal of Advanced Computer Science and Applications}, number = {1}, issn = {2158-107X}, doi = {10.14569/IJACSA.2016.070179}, pages = {571 -- 583}, abstract = {We present an approach for verifying Statecharts including infinite data spaces. We devise a technique for checking that a formula of the universal fragment of CTL is satisfied by a specification written as a Statechart. The approach is based on a property-preserving abstraction technique that additionally preserves structure. It is prototypically implemented in a logic-based framework using a theorem prover and a model checker. This paper reports on the following results. (1) We present a proof infra-structure for Statecharts in the theorem prover Isabelle/HOL, which constitutes a basis for defining a mechanised data abstraction process. The formalisation is based on Hierarchical Automata (HA) which allow a structural decomposition of Statecharts into Sequential Automata. (2) Based on this theory we introduce a data abstraction technique, which can be used to abstract the data space of a HA for a given abstraction function. The technique is based on constructing over-approximations. It is structure-preserving and is designed in a compositional way. (3) For reasons of practicability, we finally present two tactics supporting the abstraction that we have implemented in Isabelle/HOL. To make proofs more efficient, these tactics use the model checker SMV checking abstract models automatically.}, language = {en} }