Synthesis and stochastic assessment of schedules for lacquer production

H.C. Bohnenkamp, H. Hermanns, J. Klaren, Angelika H. Mader, Y.S. Usenko

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    44 Downloads (Pure)

    Abstract

    The MODEST modeling language pairs modeling features from stochastic process algebra and from timed and probabilistic automata with light-weight notations such as exception handling. It is supported by the MOTOR tool, which facilitates the execution and evaluation of MODEST specifications by means of the discrete event simulation engine of the MÖBIUS tool. This paper describes the application of MODEST, MOTOR and MÖBIUS to a highly nontrivial case. We investigate the eect of faulty behavior on a hard real-time scheduling problem from the domain of lacquer production. The scheduling problem is first solved using the timed model-checker UPPAAL. The resulting schedules are then embedded in a MODEST failure model of the lacquer production line, and analyzed with the discrete event simulator of MÖBIUS. This approach allows one to assess the quality of the schedules with respect to timeliness, utilization of resources, and sensitivity to dierent assumptions about the reliability of the production line.
    Original languageUndefined
    Title of host publicationFirst International Conference on Quantitative Evaluation of Systems (QEST 2004)
    Place of PublicationLos Alamitos, California
    PublisherIEEE Computer Science Press
    Pages28-37
    Number of pages10
    ISBN (Print)0-7695-2185-1
    DOIs
    Publication statusPublished - Sep 2004
    Event1st International Conference on Quantitative Evaluation of Systems, QEST 2004 - University of Twente, Enschede, Netherlands
    Duration: 27 Sep 200430 Sep 2004
    Conference number: 1
    http://www.qest.org/qest2004/

    Publication series

    Name
    PublisherIEEE Computer Science Press

    Conference

    Conference1st International Conference on Quantitative Evaluation of Systems, QEST 2004
    Abbreviated titleQEST
    CountryNetherlands
    CityEnschede
    Period27/09/0430/09/04
    Internet address

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-PM: PROBABILISTIC METHODS
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • IR-48991
    • METIS-220880
    • EWI-760

    Cite this

    Bohnenkamp, H. C., Hermanns, H., Klaren, J., Mader, A. H., & Usenko, Y. S. (2004). Synthesis and stochastic assessment of schedules for lacquer production. In First International Conference on Quantitative Evaluation of Systems (QEST 2004) (pp. 28-37). Los Alamitos, California: IEEE Computer Science Press. https://doi.org/10.1109/QEST.2004.10042, https://doi.org/10.1109/QEST.2004.1348013
    Bohnenkamp, H.C. ; Hermanns, H. ; Klaren, J. ; Mader, Angelika H. ; Usenko, Y.S. / Synthesis and stochastic assessment of schedules for lacquer production. First International Conference on Quantitative Evaluation of Systems (QEST 2004). Los Alamitos, California : IEEE Computer Science Press, 2004. pp. 28-37
    @inproceedings{68dc4ca317834e32863f077c9507033b,
    title = "Synthesis and stochastic assessment of schedules for lacquer production",
    abstract = "The MODEST modeling language pairs modeling features from stochastic process algebra and from timed and probabilistic automata with light-weight notations such as exception handling. It is supported by the MOTOR tool, which facilitates the execution and evaluation of MODEST specifications by means of the discrete event simulation engine of the M{\"O}BIUS tool. This paper describes the application of MODEST, MOTOR and M{\"O}BIUS to a highly nontrivial case. We investigate the eect of faulty behavior on a hard real-time scheduling problem from the domain of lacquer production. The scheduling problem is first solved using the timed model-checker UPPAAL. The resulting schedules are then embedded in a MODEST failure model of the lacquer production line, and analyzed with the discrete event simulator of M{\"O}BIUS. This approach allows one to assess the quality of the schedules with respect to timeliness, utilization of resources, and sensitivity to dierent assumptions about the reliability of the production line.",
    keywords = "FMT-MC: MODEL CHECKING, FMT-PM: PROBABILISTIC METHODS, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, IR-48991, METIS-220880, EWI-760",
    author = "H.C. Bohnenkamp and H. Hermanns and J. Klaren and Mader, {Angelika H.} and Y.S. Usenko",
    note = "Imported from DIES",
    year = "2004",
    month = "9",
    doi = "10.1109/QEST.2004.10042",
    language = "Undefined",
    isbn = "0-7695-2185-1",
    publisher = "IEEE Computer Science Press",
    pages = "28--37",
    booktitle = "First International Conference on Quantitative Evaluation of Systems (QEST 2004)",

    }

    Bohnenkamp, HC, Hermanns, H, Klaren, J, Mader, AH & Usenko, YS 2004, Synthesis and stochastic assessment of schedules for lacquer production. in First International Conference on Quantitative Evaluation of Systems (QEST 2004). IEEE Computer Science Press, Los Alamitos, California, pp. 28-37, 1st International Conference on Quantitative Evaluation of Systems, QEST 2004, Enschede, Netherlands, 27/09/04. https://doi.org/10.1109/QEST.2004.10042, https://doi.org/10.1109/QEST.2004.1348013

    Synthesis and stochastic assessment of schedules for lacquer production. / Bohnenkamp, H.C.; Hermanns, H.; Klaren, J.; Mader, Angelika H.; Usenko, Y.S.

    First International Conference on Quantitative Evaluation of Systems (QEST 2004). Los Alamitos, California : IEEE Computer Science Press, 2004. p. 28-37.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Synthesis and stochastic assessment of schedules for lacquer production

    AU - Bohnenkamp, H.C.

    AU - Hermanns, H.

    AU - Klaren, J.

    AU - Mader, Angelika H.

    AU - Usenko, Y.S.

    N1 - Imported from DIES

    PY - 2004/9

    Y1 - 2004/9

    N2 - The MODEST modeling language pairs modeling features from stochastic process algebra and from timed and probabilistic automata with light-weight notations such as exception handling. It is supported by the MOTOR tool, which facilitates the execution and evaluation of MODEST specifications by means of the discrete event simulation engine of the MÖBIUS tool. This paper describes the application of MODEST, MOTOR and MÖBIUS to a highly nontrivial case. We investigate the eect of faulty behavior on a hard real-time scheduling problem from the domain of lacquer production. The scheduling problem is first solved using the timed model-checker UPPAAL. The resulting schedules are then embedded in a MODEST failure model of the lacquer production line, and analyzed with the discrete event simulator of MÖBIUS. This approach allows one to assess the quality of the schedules with respect to timeliness, utilization of resources, and sensitivity to dierent assumptions about the reliability of the production line.

    AB - The MODEST modeling language pairs modeling features from stochastic process algebra and from timed and probabilistic automata with light-weight notations such as exception handling. It is supported by the MOTOR tool, which facilitates the execution and evaluation of MODEST specifications by means of the discrete event simulation engine of the MÖBIUS tool. This paper describes the application of MODEST, MOTOR and MÖBIUS to a highly nontrivial case. We investigate the eect of faulty behavior on a hard real-time scheduling problem from the domain of lacquer production. The scheduling problem is first solved using the timed model-checker UPPAAL. The resulting schedules are then embedded in a MODEST failure model of the lacquer production line, and analyzed with the discrete event simulator of MÖBIUS. This approach allows one to assess the quality of the schedules with respect to timeliness, utilization of resources, and sensitivity to dierent assumptions about the reliability of the production line.

    KW - FMT-MC: MODEL CHECKING

    KW - FMT-PM: PROBABILISTIC METHODS

    KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

    KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    KW - IR-48991

    KW - METIS-220880

    KW - EWI-760

    U2 - 10.1109/QEST.2004.10042

    DO - 10.1109/QEST.2004.10042

    M3 - Conference contribution

    SN - 0-7695-2185-1

    SP - 28

    EP - 37

    BT - First International Conference on Quantitative Evaluation of Systems (QEST 2004)

    PB - IEEE Computer Science Press

    CY - Los Alamitos, California

    ER -

    Bohnenkamp HC, Hermanns H, Klaren J, Mader AH, Usenko YS. Synthesis and stochastic assessment of schedules for lacquer production. In First International Conference on Quantitative Evaluation of Systems (QEST 2004). Los Alamitos, California: IEEE Computer Science Press. 2004. p. 28-37 https://doi.org/10.1109/QEST.2004.10042, https://doi.org/10.1109/QEST.2004.1348013