Contract-based specification of embedded control systems

Oǧuzcan Oguz

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    186 Downloads (Pure)

    Abstract

    In this thesis our overall aim is to provide a contract-based embedded system development process with an emphasis on specification and analysis.
    We specify components and layers via assume/guarantee contracts and use a contract algebra as the backbone to supply necessary operations to compose, refine and validate contracts.
    We employ various modelling formalisms, such as timed automata and hybrid automata to express contracts.
    The choice of the formalism is made according to the sort of behaviours of the component at hand.
    We employ appropriate model-based analysis methods, such as model checking and simulation, to support practical contract operations.

    Our first contribution is a contract-based specification architecture and the associated process.
    The specification architecture is mode based where a system is specified with a number of operational modes and a mode-switching logic.
    The concrete formalisms used are based on timed automata for switching logic and hybrid automata for specification of individual modes.
    Practical methods for composing and analysing hybrid automata-based contracts are defined over using hybrid observers which enable employing hybrid system simulation tools.
    To analyse timed automata-based contracts in isolation, model checking is employed.
    Specific validity criteria for mode and switching components are defined for each step of the specification process.

    Our second contribution is a method to use timed automata-based specifications as observers in a hybrid system simulation tool.
    We provide the associated implementation which employs Uppaal model-checking tool to execute such generic timed automata-based specifications alongside hybrid automata based-observer specifications.
    In the context of the described specification process, this enables validating contracts with assertions expressed in both timed and hybrid automata.

    Our third contribution is a generic schedulability framework using model checking on timed-CSP models.
    The framework enables analysing multiprocessor schedulability of CSP models with non-preemptive fixed-priority tasks with variable execution times.
    We present a schedulability analysis workflow that describes how to utilize the proposed framework in a generic CSP-based design process.
    We also describe how to integrate the schedulability framework to a contract-based design process.


    Original languageEnglish
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • van de Pol, Jaco , Supervisor
    • Broenink, Jan, Co-Supervisor
    • Mader, Angelika H., Co-Supervisor
    Award date16 Feb 2018
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-4497-9
    DOIs
    Publication statusPublished - 16 Feb 2018

    Fingerprint

    Specifications
    Control systems
    Model checking
    Hybrid systems
    Embedded systems
    Algebra
    Concretes

    Cite this

    Oguz, Oǧuzcan. / Contract-based specification of embedded control systems. Enschede : University of Twente, 2018. 216 p.
    @phdthesis{650d16ebb6124322b00f44dd1c31ed14,
    title = "Contract-based specification of embedded control systems",
    abstract = "In this thesis our overall aim is to provide a contract-based embedded system development process with an emphasis on specification and analysis. We specify components and layers via assume/guarantee contracts and use a contract algebra as the backbone to supply necessary operations to compose, refine and validate contracts. We employ various modelling formalisms, such as timed automata and hybrid automata to express contracts. The choice of the formalism is made according to the sort of behaviours of the component at hand. We employ appropriate model-based analysis methods, such as model checking and simulation, to support practical contract operations. Our first contribution is a contract-based specification architecture and the associated process. The specification architecture is mode based where a system is specified with a number of operational modes and a mode-switching logic. The concrete formalisms used are based on timed automata for switching logic and hybrid automata for specification of individual modes. Practical methods for composing and analysing hybrid automata-based contracts are defined over using hybrid observers which enable employing hybrid system simulation tools. To analyse timed automata-based contracts in isolation, model checking is employed. Specific validity criteria for mode and switching components are defined for each step of the specification process. Our second contribution is a method to use timed automata-based specifications as observers in a hybrid system simulation tool. We provide the associated implementation which employs Uppaal model-checking tool to execute such generic timed automata-based specifications alongside hybrid automata based-observer specifications. In the context of the described specification process, this enables validating contracts with assertions expressed in both timed and hybrid automata. Our third contribution is a generic schedulability framework using model checking on timed-CSP models. The framework enables analysing multiprocessor schedulability of CSP models with non-preemptive fixed-priority tasks with variable execution times. We present a schedulability analysis workflow that describes how to utilize the proposed framework in a generic CSP-based design process. We also describe how to integrate the schedulability framework to a contract-based design process.",
    author = "Oǧuzcan Oguz",
    note = "CTIT Ph.D. thesis series no. 17-450",
    year = "2018",
    month = "2",
    day = "16",
    doi = "10.3990/1.9789036544979",
    language = "English",
    isbn = "978-90-365-4497-9",
    publisher = "University of Twente",
    address = "Netherlands",
    school = "University of Twente",

    }

    Contract-based specification of embedded control systems. / Oguz, Oǧuzcan.

    Enschede : University of Twente, 2018. 216 p.

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    TY - THES

    T1 - Contract-based specification of embedded control systems

    AU - Oguz, Oǧuzcan

    N1 - CTIT Ph.D. thesis series no. 17-450

    PY - 2018/2/16

    Y1 - 2018/2/16

    N2 - In this thesis our overall aim is to provide a contract-based embedded system development process with an emphasis on specification and analysis. We specify components and layers via assume/guarantee contracts and use a contract algebra as the backbone to supply necessary operations to compose, refine and validate contracts. We employ various modelling formalisms, such as timed automata and hybrid automata to express contracts. The choice of the formalism is made according to the sort of behaviours of the component at hand. We employ appropriate model-based analysis methods, such as model checking and simulation, to support practical contract operations. Our first contribution is a contract-based specification architecture and the associated process. The specification architecture is mode based where a system is specified with a number of operational modes and a mode-switching logic. The concrete formalisms used are based on timed automata for switching logic and hybrid automata for specification of individual modes. Practical methods for composing and analysing hybrid automata-based contracts are defined over using hybrid observers which enable employing hybrid system simulation tools. To analyse timed automata-based contracts in isolation, model checking is employed. Specific validity criteria for mode and switching components are defined for each step of the specification process. Our second contribution is a method to use timed automata-based specifications as observers in a hybrid system simulation tool. We provide the associated implementation which employs Uppaal model-checking tool to execute such generic timed automata-based specifications alongside hybrid automata based-observer specifications. In the context of the described specification process, this enables validating contracts with assertions expressed in both timed and hybrid automata. Our third contribution is a generic schedulability framework using model checking on timed-CSP models. The framework enables analysing multiprocessor schedulability of CSP models with non-preemptive fixed-priority tasks with variable execution times. We present a schedulability analysis workflow that describes how to utilize the proposed framework in a generic CSP-based design process. We also describe how to integrate the schedulability framework to a contract-based design process.

    AB - In this thesis our overall aim is to provide a contract-based embedded system development process with an emphasis on specification and analysis. We specify components and layers via assume/guarantee contracts and use a contract algebra as the backbone to supply necessary operations to compose, refine and validate contracts. We employ various modelling formalisms, such as timed automata and hybrid automata to express contracts. The choice of the formalism is made according to the sort of behaviours of the component at hand. We employ appropriate model-based analysis methods, such as model checking and simulation, to support practical contract operations. Our first contribution is a contract-based specification architecture and the associated process. The specification architecture is mode based where a system is specified with a number of operational modes and a mode-switching logic. The concrete formalisms used are based on timed automata for switching logic and hybrid automata for specification of individual modes. Practical methods for composing and analysing hybrid automata-based contracts are defined over using hybrid observers which enable employing hybrid system simulation tools. To analyse timed automata-based contracts in isolation, model checking is employed. Specific validity criteria for mode and switching components are defined for each step of the specification process. Our second contribution is a method to use timed automata-based specifications as observers in a hybrid system simulation tool. We provide the associated implementation which employs Uppaal model-checking tool to execute such generic timed automata-based specifications alongside hybrid automata based-observer specifications. In the context of the described specification process, this enables validating contracts with assertions expressed in both timed and hybrid automata. Our third contribution is a generic schedulability framework using model checking on timed-CSP models. The framework enables analysing multiprocessor schedulability of CSP models with non-preemptive fixed-priority tasks with variable execution times. We present a schedulability analysis workflow that describes how to utilize the proposed framework in a generic CSP-based design process. We also describe how to integrate the schedulability framework to a contract-based design process.

    U2 - 10.3990/1.9789036544979

    DO - 10.3990/1.9789036544979

    M3 - PhD Thesis - Research UT, graduation UT

    SN - 978-90-365-4497-9

    PB - University of Twente

    CY - Enschede

    ER -