Change search
Refine search result
1 - 29 of 29
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the 'Create feeds' function.
  • 1.
    Chen, DeJiu
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Embedded Control Systems.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Östberg, Kenneth
    SP Technical Research Institute of Sweden.
    Asplund, Fredrik
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Embedded Control Systems.
    Baumann, Christoph
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A Knowledge-in-the-Loop Approach to Integrated Safety&Security for Cooperative System-of-Systems2015In: IEEE Seventh International Conference on Intelligent Computing and Information Systems, IEEE , 2015Conference paper (Refereed)
    Abstract [en]

    A system-of-systems (SoS) is inherently open inconfiguration and evolutionary in lifecycle. For the nextgeneration of cooperative cyber-physical system-of-systems,safety and security constitute two key issues of public concernthat affect the deployment and acceptance. In engineering, theopenness and evolutionary nature also entail radical paradigmshifts. This paper presents one novel approach to thedevelopment of qualified cyber-physical system-of-systems, withCooperative Intelligent Transport Systems (C-ITS) as one target.The approach, referred to as knowledge-in-the-loop, aims toallow a synergy of well-managed lifecycles, formal qualityassurance, and smart system features. One research goal is toenable an evolutionary development with continuous andtraceable flows of system rationale from design-time to postdeploymenttime and back, supporting automated knowledgeinference and enrichment. Another research goal is to develop aformal approach to risk-aware dynamic treatment of safety andsecurity as a whole in the context of system-of-systems. Key basetechnologies include: (1) EAST-ADL for the consolidation ofsystem-wide concerns and for the creation of an ontology foradvanced run-time decisions, (2) Learning Based-Testing for runtimeand post-deployment model inference, safety monitoringand testing, (3) Provable Isolation for run-time attack detectionand enforcement of security in real-time operating systems.

  • 2.
    Feng, Lei
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Lundmark, Simon
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Mudassar A.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Wong, Peter Y. H.
    Case studies in learning-based testing2013In: Testing Software and Systems: 25th IFIP WG 6.1 International Conference, ICTSS 2013, Istanbul, Turkey, November 13-15, 2013, Proceedings, Springer, 2013, p. 164-179Conference paper (Refereed)
    Abstract [en]

    We present case studies which show how the paradigm of learning-based testing (LBT) can be successfully applied to black-box requirements testing of industrial reactive systems. For this, we apply a new testing tool LBTest, which combines algorithms for incremental black-box learning of Kripke structures with model checking technology. We show how test requirements can be modeled in propositional linear temporal logic extended by finite data types.We then provide benchmark performance results for LBTest applied to three industrial case studies.

  • 3.
    Feng, Lei
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Wong, Peter Y. H.
    SDL Fredhopper.
    Case Studies in Learning-based Testing2013Report (Other academic)
    Abstract [en]

    We present case studies which show how the paradigm of learning-based testing (LBT) can be successfully applied to black-box requirements testing of reactive systems. For this we apply a new testing tool LBTest, which combines algorithms for incremental black-box learning of Kripke structures with model checking technology. We show how test requirements can be modeled in propositional linear temporal logic extended by finite abstract data types. We provide benchmark performance results for LBTest applied to two industrial case studies. Finally we present a first coverage study for the tool.

  • 4. Howar, Falk
    et al.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Rausch, Andreas
    Learning Systems: Machine-Learning in Software Products and Learning-Based Analysis of Software Systems Special Track at ISoLA 20162016In: LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, p. 651-654Conference paper (Refereed)
  • 5. Hu, S.
    et al.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dynamic-measurement modeling of attitude motion for N-bodies spacecraft with applications2011In: Proceedings of the 30th Chinese Control Conference, 2011, p. 1453-1458Conference paper (Refereed)
    Abstract [en]

    Modeling analysis technique is one of the most important means in processing spaceflight mission. In this paper, the graph based description is given, and a series of dynamic-measurement system models are built for the attitude motion of a N-bodies spacecraft, which include the states evolvement equation of the main body, the states evolvement equations of the accessories, the inertia based measurement equations and the celestial bodies based measurement equation and the GPS based measurement equations of attitudes of the N-bodies etc.. These models are educed with some typical methods of theoretical analysis and dynamic description and are simplified into linearized discrete equations. At the end of the paper some valuable applications are pointed out.

  • 6.
    Hu, Shaolin
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. Nanjing University of Science and Technology, China .
    Chen, R.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huajiang, O.
    Dynamic-measurement system modeling of spinning spacecraft attitude and their applications2007In: Chinese Space Science and Technology, ISSN 1000-758X, Vol. 27, no 4, p. 1-6+20Article in journal (Refereed)
    Abstract [en]

    The modeling analysis technique is one of the most important approaches in space-flight mission. Based on the dynamical analysis, the copling models of the attitudes with angle velocities were successfully decoupled into two series independently differential equations. And, these two series models were integrated into an extended dynamic-measurement system with joint relationship equations. This new integrated model could be widely used in attitude determination, attitude control and attitude monitoring of the spinning spacecraft. Based on this integrated model, a series of practical algorithms were described to estimate attitude as well as spinning angles velocities with high precision.

  • 7.
    Hu, Shaolin
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. Nanjing University of Science and Technology, China .
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Chen, R.
    Fault-tolerant design of computer cyclic check and control system2007In: Proceedings of the 26th Chinese Control Conference, CCC 2007, 2007, p. 426-430Conference paper (Refereed)
    Abstract [en]

    Computer Cyclic Check is widely used in many different fields. Some limitations as well as bugs of classical algorithms in the computer cyclic check system are analyzed in detailed. In order to overcome these advantages, two series of new algorithms are set up in this paper, one of which is built for the computer cyclic check system with fixed reference value and the other for the computer cyclic check under operation steering with variant directive trajectory. Theoretical analysis and simulation result shows that these new algorithms are fault-tolerant and safe. These new algorithms can be widely used in engineering to improve safety of computer cyclic check system.

  • 8.
    Hu, Shaolin
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Chen, R. -S
    Fault-tolerant algorithm of signal reconstruction in computer controlled systems2006In: Xitong Fangzhen Xuebao / Journal of System Simulation, ISSN 1004-731X, Vol. 18, no SUPPL. 2, p. 841-843Article in journal (Refereed)
    Abstract [en]

    Signal reconstruction is an important step in communication between the computer controlled system and computer system. Based on the famous Shannon reconstructing theory, some classical algorithms (such as ZOH algorithm and 1-order reconstruction algorithm, etc.) were analyzed and some shortages of these algorithms were pointed out. And, a new practical 1-step fault-tolerant prediction algorithm was set up. In order to realize this fault-tolerant algorithm, the three-points-interpolation algorithm was combined into the reconstruction process. This new algorithm has the ability to overcome bad influence from outliers and has very simple computing complexity. So, this algorithm can be safely used in on-line control.

  • 9.
    Hu, Shaolin
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Chen, Rushan
    Huajiang, Ouyang
    Iterative estimators of parameters in linear models with partially variant coefficients2007In: International Journal of Applied Mathematics and Computer Sciences, ISSN 1307-6906, Vol. 17, no 2, p. 179-187Article in journal (Refereed)
    Abstract [en]

    A new kind of linear model with partially variant coefficients is proposed and a series of iterative algorithms are introduced and verified. The new generalized linear model includes the ordinary linear regression model as a special case. The iterative algorithms efficiently overcome some difficulties in computation with multidimensional inputs and incessantly appending parameters. An important application is described at the end of this article, which shows that this new model is reasonable and applicable in practical fields.

  • 10.
    Meinke, Karl
    KTH, Superseded Departments, Numerical Analysis and Computer Science, NADA.
    automated black-box testing of functional correctness using function approximation2004In: ISSTA 2004 - Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, 2004, p. 143-153Conference paper (Refereed)
    Abstract [en]

    We consider black-box testing of functional correctness as a special case of a satisfiability or constraint solving problem. We introduce a general method for solving this problem based on function approximation. We then describe some practical results obtained for an automated testing algorithm using approximation by piecewise polynomial functions.

  • 11.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    CGE: A sequential learning algorithm for mealy automata2010In: Grammatical Inference: Theoretical Results and Applications 10th International Colloquium, ICGI 2010, Valencia, Spain, September 13-16, 2010. Proceedings / [ed] José M. Sempere and Pedro García, 2010, p. 148-162Conference paper (Refereed)
    Abstract [en]

    We introduce a new algorithm for sequential learning of Mealy automata by congruence generator extension (CGE). Our approach makes use of techniques from term rewriting theory and universal algebra for compactly representing and manipulating automata using finite congruence generator sets represented as string rewriting systems (SRS). We prove that the CGE algorithm correctly learns in the limit.

  • 12.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Learning-Based testing of cyber-physical systems-of-systems: A platooning study2017In: 14th European Workshop on Computer Performance Engineering, EPEW 2017, Springer, 2017, Vol. 10497, p. 135-151Conference paper (Refereed)
    Abstract [en]

    Learning-based testing (LBT) is a paradigm for fully automated requirements testing that combines machine learning with model-checking techniques. LBT has been shown to be effective for unit and integration testing of safety critical components in cyber-physical systems, e.g. automotive ECU software. We consider the challenges faced, and some initial results obtained in an effort to scale up LBT to testing co-operative open cyber-physical systems-of-systems (CO-CPS). For this we focus on a case study of testing safety and performance properties of multi-vehicle platoons.

  • 13.
    Meinke, Karl
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Learning-Based Testing of Cyber-Physical Systems-of-Systems: A Platooning Study2017In: / [ed] Reinecke P., Di Marco A., 2017, Vol. 10497, p. 135-151Conference paper (Refereed)
    Abstract [en]

    Learning-based testing (LBT) is a paradigm for fully automated requirements testing that combines machine learning withmodel-checking techniques. LBT has been shown to be effective for unit and integrationtesting of safety critical components in cyber-physical systems, e.g. automotive ECU software.We consider the challenges faced, and some initial results obtained in an effort to scale up LBTto testing co-operative open cyber-physical systems-of-systems (CO-CPS).For this we focus on a case study of testing safety and performance properties of multi-vehicle platoons.

  • 14.
    Meinke, Karl
    KTH, Superseded Departments, Numerical Analysis and Computer Science, NADA.
    Proof theory of higher-order equations: conservativity, normal forms and term rewriting2003In: Journal of computer and system sciences (Print), ISSN 0022-0000, E-ISSN 1090-2724, Vol. 67, no 1, p. 127-173Article in journal (Refereed)
    Abstract [en]

    We introduce a necessary and sufficient condition for the omega-extensionality rule of higher-order equational logic to be conservative over first-order many-sorted equational logic for ground first-order equations. This gives a precise condition under which computation in the higher-order initial model by term rewriting is possible. The condition is then generalised to characterise a normal form for higher-order equational proofs in which extensionality inferences occur only as the final proof inferences. The main result is based on a notion of observational equivalence between higher-order elements induced by a topology of finite information on such elements. Applied to extensional higher-order algebras with countable first-order carrier sets, the finite information topology is metric and second countable in every type.

  • 15.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A Learning-based Approach to Unit Testing of Numerical Software2010In: 22nd IFIPInternational Conference on Testing Software and Systems, Natal, Brazil, Nov. 8-12, 2010 / [ed] Alexandre Petrenko, Adenilso da Silva Simão, José Carlos Maldonado, Berlin, Heidelberg: Springer , 2010, p. 221-235Conference paper (Refereed)
    Abstract [en]

    We present an application of learning-based testing to theproblem of automated test case generation (ATCG) for numerical soft-ware. Our approach uses n-dimensional polynomial models as an algo-rithmically learned abstraction of the SUT which supports n-wise testing.Test cases are iteratively generated by applying a satisfiability algorithmto first-order program specifications over real closed fields and iterativelyrefined piecewise polynomial models.We benchmark the performance of our iterative ATCG algorithm againstiterative random testing, and empirically analyse its performance in find-ing injected errors in numerical codes. Our results show that for softwarewith small errors, or long mean time to failure, learning-based testing isincreasingly more efficient than iterative random testing.

  • 16.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    An incremental learning algorithm for extended mealy automata2012In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I / [ed] Tiziana Margaria, Bernhard Steffen, Springer, 2012, no PART 1, p. 488-504Conference paper (Refereed)
    Abstract [en]

    We present a new algorithm ICGE for incremental learning of extended Mealy automata computing over abstract data types. Our approach extends and refines our previous research on congruence generator extension (CGE) as an algebraic approach to automaton learning. In the congruence generator approach, confluent terminating string rewriting systems (SRS) are used to represent hypothesis automata. We show how an approximating sequence R 0 , R 1 , ... of confluent terminating SRS can be directly and incrementally generated from observations about the loop structure of an unknown automaton A. Such an approximating sequence converges finitely if A is finite state, and converges in the limit if A is an infinite state automaton.

  • 17.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Learning-Based Testing for Reactive Systems using Term Rewriting Technology2011In: Proceedings of the 22nd IFIP International Conference on Testing Software and Systems, Paris, France, November 7-9, 2011 / [ed] B. Wolff and F. Zaidi, Berlin, Heidelberg: Springer , 2011, p. 97-114Conference paper (Refereed)
    Abstract [en]

    We show how the paradigm of learning-based testing (LBT) can be applied to automate specification-based black-box testing of reactive systems using term rewriting technology. A general model for a reactive system can be given by an extended Mealy automata (EMA) over an abstract data type (ADT).A finite state EMA over an ADT can be efficiently learned in polynomial time using the CGE regular inference algorithm, which builds a compact representation as a complete term rewriting system. We show how this rewriting system can be used to model check the learned automaton against a temporal logic specification by means of narrowing. Combining CGE learning with a narrowing model checker we obtain a new and general architecture for learning-based testing of reactive systems. We compare the performance of this LBT architecture against random testing using a case study.

  • 18.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Learning-based software testing: A tutorial2012In: Leveraging Applications of Formal Methods, Verification, and Validation: International Workshops, SARS 2011 and MLSC 2011, Held Under the Auspices of ISoLA 2011 in Vienna, Austria, October 17-18, 2011. Revised Selected Papers / [ed] Reiner Hähnle, Jens Knoop, Tiziana Margaria, Dietmar Schreiner, Bernhard Steffen, Springer, 2012, p. 200-219Conference paper (Refereed)
    Abstract [en]

    We present an overview of the paradigm of learning-based testing (LBT) for software systems. LBT is a fully automated method for specification-based black-box testing using computational learning principles. It applies the principle of tests as queries, where queries are either generated by a learning algorithm or by a model checker through use of a formal requirements specification. LBT can be applied to automate black-box testing of a variety of different software architectures including procedural and reactive systems. We describe some different testing platforms which have been designed using this paradigm and some representative evaluation results. We also compare LBT with related testing methods.

  • 19.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nycander, Peter
    Learning-Based Testing of Distributed Microservice Architectures: Correctness and Fault Injection2015In: SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2015), 2015, p. 3-10Conference paper (Refereed)
    Abstract [en]

    We report on early results in a long term project to apply learning-based testing (LBT) to evaluate the functional correctness of distributed systems and their robustness to injected faults. We present a case study of a commercial product for counter-party credit risk implemented as a distributed microservice architecture. We describe the experimental set-up, as well as test results. From this experiment, we draw some conclusions about prospects for future research in learning-based testing.

  • 20.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    An Efficient Model Inference Algorithm for Learning-based Testing of Reactive Systems2012Report (Other academic)
    Abstract [en]

    Learning-based testing (LBT) is an emerging methodology to automate iterative black-box requirements testing of software systems. The methodology involves combining model inference with model checking techniques. However, a variety of optimisations on model inference are necessary in order to achieve scalable testing for large systems.

    In this paper we describe the IKL learning algorithm which is an active incremental learning algorithm for deterministic Kripke structures. We formally prove the correctness of IKL. We discuss the optimisations it incorporates to achieve scalability of testing. We also evaluate a black box heuristic for test termination based on convergence of IKL learning.

  • 21.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Correctness and Performance of an Incremental Learning Algorithm for Finite Automata2011Conference paper (Other academic)
    Abstract [en]

    We present a new algorithm IDS for incremental learning of deterministic finite automata (DFA). This algorithm is based on the concept of distinguishing sequences introduced in (Angluin, 1981). We give a rigorous proof that two versions of this learning algorithm correctly learn in the limit. Finally we present an empirical performance analysis that compares these two algorithms, focussing on learning times and different types of learning queries. We conclude that IDS is an efficient algorithm for software engineering applications of automata learning, such as testing and model inference.

  • 22.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Correctness and Performance of an Incremental Learning Algorithm for Finite Automata2010Report (Other academic)
    Abstract [en]

    We present a new algorithm IDSfor incremental learning of deterministic finite automata (DFA). This algorithm is based on the concept of distinguishing sequences introduced in [Angluin 1981]. We give a rigorous proof that two versions of this learning algorithm correctly learn in the limit. Finally we present an empirical performance analysis that compares these two algorithms, focussing on learning times and different types of learning queries. We conclude that IDSis an efficient algorithm for software engineering applications of automata learning, such as testing and model inference.

  • 23.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Incremental Learning based Testing for Reactive Systems2011In: / [ed] Martin Gogolla and Burkhart Wolff, 2011, p. 134-151Conference paper (Refereed)
    Abstract [en]

    We show how the paradigm of learning-based testing (LBT)can be applied to automate specification-based black-box testing of reactivesystems. Since reactive systems can be modeled as Kripke structures,we introduce an efficient incremental learning algorithm IKL forsuch structures. We show how an implementation of this algorithm combinedwith an efficient model checker such as NuSMV yields an effectivelearning-based testing architecture for automated test case generation(ATCG), execution and evaluation, starting from temporal logic requirements.

  • 24.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    LBTest: A Learning-based Testing Tool for Reactive Systems2013In: Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013, IEEE Computer Society, 2013, p. 447-454Conference paper (Refereed)
    Abstract [en]

    We give an introduction to the LBTest tool which implements learning-based testing for reactive systems. It makes use of incremental learning and model checking algorithms to automate: i) test case generation, ii) test execution and iii) test verdict construction. The paper illustrates the tool by means of a pedagogical case study, to enable the user to setup and learn the tool quickly. We provide a usability exercise to support tool evaluation.

  • 25.
    Meinke, Karl
    et al.
    KTH, Superseded Departments, Numerical Analysis and Computer Science, NADA.
    Steggles, L. J.
    Correctness of dataflow and systolic algorithms using algebras of streams2001In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 38, no 1, p. 45-88Article in journal (Refereed)
    Abstract [en]

    We present two case studies which illustrate the use of second-order algebra as a formalism for specification and verification of hardware algorithms. In the first case study we specify a systolic algorithm for convolution and formally verify its correctness using second-order equational logic. The second case study demonstrates the expressive power of second-order algebraic specifications by presenting a non-constructive specification of the Hamming stream problem. A dataflow algorithm for computing the Hamming stream is then specified and the correctness of this algorithm is verified by semantical methods. Both case studies illustrate aspects of the metatheory of second-order equational logic.

  • 26.
    Meinke, Karl
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Walkinshaw, N.
    Model-based testing and model inference2012In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I / [ed] Tiziana Margaria, Bernhard Steffen, Springer, 2012, no PART 1, p. 440-443Conference paper (Refereed)
    Abstract [en]

    Model-based software testing is well established, and can be traced back to Moore's "Gedanken experiments" on finite state machines from 1956 [10]. The best known approaches involve the use of models (such as UML interaction diagrams or state machines) as the basis for selecting test inputs that seek to explore the core functionality of the system. Outputs from the test executions can subsequently be checked against the model.

  • 27. Shaolin, Hu
    et al.
    Xiaofeng, Wang
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
    Huajiang, Ouyang
    Outlier- tolerant fitting and online diagnosis of outliers in dynamic process sampling data series2011In: 3rd International Conference on Artificial Intelligence and Computational Intelligence, AICI 2011, 2011, p. 195-203Conference paper (Refereed)
    Abstract [en]

    Outliers as well as outlier patches, which widely emerge in dynamic process sampling data series, have strong bad influence on signal processing. In this paper, a series of recursive outlier-tolerant fitting algorithms are built to fit reliably the trajectories of a non-stationary sampling process when there are some outliers arising from output components of the process. Based on the recursive outlier-tolerant fitting algorithms stated above, a series of practical programs are given to online detect outliers in dynamic process and to identify magnitudes of these outliers as well as outlier patches. Simulation results show that these new methods are efficient.

  • 28.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Incremental Learning and Testing of Reactive Systems2011Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis concerns the design, implementation and evaluation of a specification based testing architecture for reactive systems using the paradigm of learning-based testing. As part of this work we have designed, verified and implemented new incremental learning algorithms for DFA and Kripke structures.These have been integrated with the NuSMV model checker to give a new learning-based testing architecture. We have evaluated our architecture on case studies and shown that the method is effective.

  • 29. Wong, Peter Y. H.
    et al.
    Bubel, Richard
    de Boer, Frank S.
    Gómez-Zamalloa, Miguel
    de Gouw, Stijn
    Hähnle, Reiner
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Mudassar A.
    Testing abstract behavioral specifications2014In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 17, no 1, p. 107-119Article in journal (Refereed)
    Abstract [en]

    We present a range of testing techniques for the Abstract Behavioral Specification (ABS) language and apply them to an industrial case study. ABS is a formal modeling language for highly variable, concurrent, component-based systems. The nature of these systems makes them susceptible to the introduction of subtle bugs that are hard to detect in the presence of steady adaptation. While static analysis techniques are available for an abstract language such as ABS, testing is still indispensable and complements analytic methods. We focus on fully automated testing techniques including black-box and glass-box test generation as well as runtime assertion checking, which are shown to be effective in an industrial setting.

1 - 29 of 29
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf