liu.seSearch for publications in DiVA
Change search
Link to record
Permanent link

Direct link
BETA
Karlsson, Daniel
Publications (10 of 12) Show all publications
Karlsson, D., Eles, P. I. & Peng , Z. (2008). Model validation for embedded systems using formal method-aided simulation. IET Computers and digital techniques, 2(6), 413-433
Open this publication in new window or tab >>Model validation for embedded systems using formal method-aided simulation
2008 (English)In: IET Computers and digital techniques, ISSN 1751-8601 , Vol. 2, no 6, p. 413-433Article in journal (Refereed) Published
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. At the same time, the systems must fulfil strict requirements on reliability and correctness. Informal validation techniques, such as simulation, suffer from the fact that they only examine a small fraction of the state space. Therefore simulation results cannot be 100% guaranteed. Formal techniques, on the other hand, suffer from state-space explosion and might not be practical for huge, complex systems due to memory and time limitations. A validation approach, based on simulation, which addresses some of the above problems is proposed. Formal methods, in particular, model checking, are used to aid, or guide, the simulation process in certain situations in order to boost coverage. The invocation frequency of the model checker is dynamically controlled by estimating certain parameters related to the simulation speed of the particular system at hand. These estimations are based on statistical data collected during the validation session, in order to minimise veri. cation time, and at the same time, achieve reasonable coverage.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-16215 (URN)10.1049/iet-cdt:20070128 (DOI)
Note
This paper is a postprint of a paper submitted to and accepted for publication in IET COMPUTERS AND DIGITAL TECHNIQUES and is subject to Institution of Engineering and Technology Copyright. The copy of record is available at IET Digital Library Original Publication: Daniel Karlsson, Petru Ion Eles and Zebo Peng, Model validation for embedded systems using formal method-aided simulation, 2008, IET COMPUTERS AND DIGITAL TECHNIQUES, (2), 6, 413-433. http://dx.doi.org/10.1049/iet-cdt:20070128 Copyright: Iet http://www.theiet.org/ Available from: 2009-01-15 Created: 2009-01-09 Last updated: 2009-05-04Bibliographically approved
Karlsson, D., Eles, P. I. & Peng, Z. (2008). Transactor-based Formal Verification of Real-time Embedded Systems (1ed.). In: D. Karlsson,Z. Peng ,P. Eles (Ed.), Embedded Systems Specification and Design Languages: (pp. 255-270). Dordrecht, Netherlands: Springer
Open this publication in new window or tab >>Transactor-based Formal Verification of Real-time Embedded Systems
2008 (English)In: Embedded Systems Specification and Design Languages / [ed] D. Karlsson,Z. Peng ,P. Eles, Dordrecht, Netherlands: Springer , 2008, 1, p. 255-270Chapter in book (Other academic)
Abstract [en]

  With the increasing complexity of today-s embedded systems, there is a need to formally verify such designs at mixed abstraction levels. This is needed if some components are described at high levels of abstraction, whereas others are described at low levels. Components in single abstraction level designs communicate through channels, which capture essential features of the communication. If the connected components communicate at different abstraction levels, then these channels are replaced with transactors that translate requests back and forth between the abstraction levels. It is important that the transactor still preserves the external characteristics, e.g. timing, of the original channel. This chapter proposes a technique to generate such transactors. According to this technique, transactors are specified in a single formal language, which is capable of capturing timing aspects. The approach is especially targeted to formal verification.

Place, publisher, year, edition, pages
Dordrecht, Netherlands: Springer, 2008 Edition: 1
Series
Lecture Notes in Electrical Engineering ; 10
Keywords
embedded systems, formal verification, component communication, abstraction levels, transactor, single formal language
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-43978 (URN)10.1007/978-1-4020-8297-9_18 (DOI)75285 (Local ID)978-1-4020-8296-2 (ISBN)978-1-4020-8297-9 (ISBN)75285 (Archive number)75285 (OAI)
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2018-01-12Bibliographically approved
Karlsson, D., Eles, P. I. & Peng, Z. (2007). Formal verification of component-based designs. Design automation for embedded systems, 11(1), 49-90
Open this publication in new window or tab >>Formal verification of component-based designs
2007 (English)In: Design automation for embedded systems, ISSN 0929-5585, E-ISSN 1572-8080, Vol. 11, no 1, p. 49-90Article in journal (Refereed) Published
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex, and designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must fulfill strict requirements on reliability and correctness. This paper proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components, each of them already formally verified by their designers. The components are considered correct given that the environment satisfies certain properties imposed by the component. The methodology verifies the correctness of the glue logic inserted between the components and the interaction of the components through the glue logic. Each such glue logic is verified one at a time using model checking techniques. Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply such a verification methodology on real-life examples. © Springer Science + Business Media, LLC 2006.

Keywords
Components, Embedded systems, Formal verification, IP, Model checking, Petri-nets, Real-time systems
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-49986 (URN)10.1007/s10617-006-9723-3 (DOI)
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2017-12-12
Larsson, E., Amirijoo, M., Karlsson, D. & Eles, P. I. (2007). What Impacts Course Evaluation?. In: 12th SIGCSE Conf. on Innovation and Technology in Computer Science Education,2007: . Paper presented at 12th SIGCSE Conf. on Innovation and Technology in Computer Science Education,2007 (pp. 333-333).
Open this publication in new window or tab >>What Impacts Course Evaluation?
2007 (English)In: 12th SIGCSE Conf. on Innovation and Technology in Computer Science Education,2007, 2007, p. 333-333Conference paper, Published paper (Refereed)
Abstract [en]

Today most universities are using course evaluations. However, course evaluations are often discussed and questioned. This paper reports on a survey where we aim at finding out (1) if students have a preconceived notion of a course, (2) if course evaluation scores can be predicted early in a course, (3) if exam throughput impacts course evaluation, and (4) if web-based evaluation reflects the general opinion from students. The results from the study indicate that students do not let preconceived notion impact nor does exam throughput matter to course evaluation. Further, the final web-based results seem to correlate with opinion of students attending lectures. However, the evaluation grades tend to be defined early in the course; hence first impression lasts.

Keywords
education, computer science, course evaluation
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-39297 (URN)10.1145/1268784.1268901 (DOI)47830 (Local ID)978-1-59593-610-3 (ISBN)47830 (Archive number)47830 (OAI)
Conference
12th SIGCSE Conf. on Innovation and Technology in Computer Science Education,2007
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2018-01-13
Karlsson, D., Eles, P. I. & Peng, Z. (2006). Formal Verification of SystemC Designs Using a Petri-Net based Representation. In: Design Automation and Test in Europe Conference DATE 2006,2006: . Paper presented at Design Automation and Test in Europe Conference DATE 2006 (pp. 1228). Munich, Germany: IEEE Computer Society Press
Open this publication in new window or tab >>Formal Verification of SystemC Designs Using a Petri-Net based Representation
2006 (English)In: Design Automation and Test in Europe Conference DATE 2006,2006, Munich, Germany: IEEE Computer Society Press , 2006, p. 1228-Conference paper, Published paper (Refereed)
Abstract [en]

This paper presents an effective approach to formally verify SystemC designs. The approach translates SystemC models into a Petri-Net based representation. The Petri-net model is then used for model checking of properties expressed in a timed temporal logic. The approach is particularly suitable for, but not restricted to, models at a high level of abstraction, such as transaction-level. The efficiency of the approach is illustrated by experiments.

Place, publisher, year, edition, pages
Munich, Germany: IEEE Computer Society Press, 2006
Keywords
formal verification, SystemC, Petri-Net representation, temporal logic, model checking, transaction-level
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-31230 (URN)10.1109/DATE.2006.244076 (DOI)16983 (Local ID)3-9810801-1-4 (ISBN)16983 (Archive number)16983 (OAI)
Conference
Design Automation and Test in Europe Conference DATE 2006
Available from: 2009-10-09 Created: 2009-10-09 Last updated: 2018-01-13
Karlsson, D. (2006). Verification of Component-based Embedded System Designs. (Doctoral dissertation). Institutionen för datavetenskap
Open this publication in new window or tab >>Verification of Component-based Embedded System Designs
2006 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components. At the same time, the systems must fulfill strict functional and non-functional requirements.

This thesis presents novel and efficient techniques for the verification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+.

Two complementary problems are addressed: component verification and integration verification. With component verification the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment.

Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of SystemC designs by translating them into the PRES+ representation. The second technique involves a simulation based approach into which formal methods are injected to boost verification efficiency.

Provided that each individual component is verified and is guaranteed to function correctly, the components are interconnected to form a complete system. What remains to be verified is the interface logic, also called glue logic, and the interaction between components.

Each glue logic and interface cannot be verified in isolation. It must be put into the context in which it is supposed to work. An appropriate environment must thus be derived from the components to which the glue logic is connected. This environment must capture the essential properties of the whole system with respect to the properties being verified. In this way, both the glue logic and the interaction of components through the glue logic are verified. The thesis presents algorithms for automatically creating such environments as well as the underlying theoretical framework and a step-by-step roadmap on how to apply these algorithms.

Place, publisher, year, edition, pages
Institutionen för datavetenskap, 2006. p. 294
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1017
Keywords
Datorsystem, embedded systems, formal verification, Petri-net, IP, reuse, components, model checking, simulation, Datorsystem
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-7473 (URN)91-85523-79-8 (ISBN)
Public defence
2006-06-19, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Opponent
Supervisors
Available from: 2006-09-28 Created: 2006-09-28 Last updated: 2009-11-25Bibliographically approved
Karlsson, D., Eles, P. I. & Peng, Z. (2005). Validation of Embedded Systems using Formal Method aided Verification. In: 8th Euromicro Conference on Digital System Design DSD2005,2005: . Paper presented at 8th Euromicro Conference on Digital System Design DSD2005 (pp. 196). Porto, Portugal: IEEE Computer Society Press
Open this publication in new window or tab >>Validation of Embedded Systems using Formal Method aided Verification
2005 (English)In: 8th Euromicro Conference on Digital System Design DSD2005,2005, Porto, Portugal: IEEE Computer Society Press , 2005, p. 196-Conference paper, Published paper (Refereed)
Abstract [en]

Informal validation techniques, such as simulation, suffer from the fact that they only examine a small fraction of the state space. Formal techniques, on the other hand, suffer from state space explosion and are not practical to use for huge, complex systems. This paper proposes a validation approach, based on simulation, which addresses some of the above problems. Formal methods, in particular model checking, are used to aid the simulation process in certain situations in order to boost coverage. The invocation frequency of the model checker is dynamically controlled by estimating certain parameters, based on statistics collected previously during the same validation session, in order to minimise verification time and at the same time achieve reasonable coverage. The approach has been demonstrated feasible by numerous experimental results.

Place, publisher, year, edition, pages
Porto, Portugal: IEEE Computer Society Press, 2005
Keywords
formal verification, validation approach, simulation, formal methods, model checker
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-28509 (URN)10.1109/DSD.2005.75 (DOI)13658 (Local ID)0-7695-2433-8 (ISBN)13658 (Archive number)13658 (OAI)
Conference
8th Euromicro Conference on Digital System Design DSD2005
Available from: 2009-10-09 Created: 2009-10-09 Last updated: 2018-01-13
Karlsson, D., Eles, P. I. & Peng, Z. (2004). A Formal Verification Approach for IP-based Designs. In: Forum on Specification and Design Languages,2004 (pp. 556-567).
Open this publication in new window or tab >>A Formal Verification Approach for IP-based Designs
2004 (English)In: Forum on Specification and Design Languages,2004, 2004, p. 556-567Conference paper, Published paper (Refereed)
Abstract [en]

This paper proposes a formal verification methodology which is smoothly integrated with component-based system-level design, using a divide and conquer approach. The methodology assumes that the system consists of several reusable components, each of them already verified by their designers and which are considered correct under the assumption that the environment satisfies certain properties assumed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques. A big difficulty with such an approach is the question how to handle the connected components and the rest of the system in the verification of the glue logic, which only constitutes a small part of the design. In this paper, algorithms for generating a model corresponding to the rest of the system are discussed together with guidelines on how and when to use them. The methodology is illustrated by a small case study on a mobile telephone.

Keywords
formal verification, component-based design, glue logic
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-23199 (URN)2610 (Local ID)2610 (Archive number)2610 (OAI)
Available from: 2009-10-07 Created: 2009-10-07 Last updated: 2018-01-13
Karlsson, D., Eles, P. I. & Peng, Z. (2004). A Formal Verification Methodology for IP-based Designs. In: EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, Architectures, Methods and Tools,2004: . Paper presented at EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, DSD 2004 (pp. 372). Rennes, France: IEEE Computer Society Press
Open this publication in new window or tab >>A Formal Verification Methodology for IP-based Designs
2004 (English)In: EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, Architectures, Methods and Tools,2004, Rennes, France: IEEE Computer Society Press , 2004, p. 372-Conference paper, Published paper (Refereed)
Abstract [en]

This paper proposes a formal verification methodology which smoothly integrates with component-based system-level design, using a divide and conquer approach. The methodology assumes that the system consists of several reusable components, each of them already verified by their designers and which are considered correct under the assumption that the environment satisfies certain properties assumed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques. Experiments, performed on a real-life example (mobile telephone), demonstrating the efficiency and intuitivity of the methodology, are moreover thoroughly presented. Three different properties have been verified on one part of the system.

Place, publisher, year, edition, pages
Rennes, France: IEEE Computer Society Press, 2004
Keywords
formal verification, component-based design, glue logic, model checking
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-23200 (URN)10.1109/DSD.2004.1333299 (DOI)2611 (Local ID)0-7695-2203-3 (ISBN)2611 (Archive number)2611 (OAI)
Conference
EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, DSD 2004
Available from: 2009-10-07 Created: 2009-10-07 Last updated: 2018-01-13
Karlsson, D. (2003). Towards Formal Verification in a Component-based Reuse Methodology. (Licentiate dissertation). : Institutionen för datavetenskap
Open this publication in new window or tab >>Towards Formal Verification in a Component-based Reuse Methodology
2003 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness.

This thesis proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components. Each of these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques.

The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis.

Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples.

Place, publisher, year, edition, pages
Institutionen för datavetenskap, 2003. p. 187
Series
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1058
Keywords
Formal verification, Model checking, Petri net, Reuse
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-5696 (URN)91-7373-787-9 (ISBN)
Presentation
2003-12-11, 00:00 (English)
Supervisors
Note
Report code: LiU-Tek-Lic-2003:57.Available from: 2003-12-05 Created: 2003-12-05 Last updated: 2018-01-13
Organisations

Search in DiVA

Show all publications