Synthesis and stochastic assessment of schedules for lacquer production

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

doi:10.1109/QEST.2004.1348013

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 proceeding › Conference contribution › Academic › peer-review

93 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 language	English
Title of host publication	First International Conference on Quantitative Evaluation of Systems (QEST 2004)
Place of Publication	Los Alamitos, California
Publisher	IEEE
Pages	28-37
Number of pages	10
ISBN (Print)	0-7695-2185-1
DOIs	https://doi.org/10.1109/QEST.2004.1348013
Publication status	Published - Sept 2004
Event	1st International Conference on Quantitative Evaluation of Systems, QEST 2004 - University of Twente, Enschede, Netherlands Duration: 27 Sept 2004 → 30 Sept 2004 Conference number: 1 http://www.qest.org/qest2004/

Conference

Conference	1st International Conference on Quantitative Evaluation of Systems, QEST 2004
Abbreviated title	QEST
Country/Territory	Netherlands
City	Enschede
Period	27/09/04 → 30/09/04
Internet address	http://www.qest.org/qest2004/

Keywords

FMT-MC: MODEL CHECKING
FMT-PM: PROBABILISTIC METHODS
FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

Access to Document

10.1109/QEST.2004.1348013

Cite this

@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",

author = "H.C. Bohnenkamp and H. Hermanns and J. Klaren and Mader, \{Angelika H.\} and Y.S. Usenko",

year = "2004",

month = sep,

doi = "10.1109/QEST.2004.1348013",

language = "English",

isbn = "0-7695-2185-1",

pages = "28--37",

booktitle = "First International Conference on Quantitative Evaluation of Systems (QEST 2004)",

publisher = "IEEE",

address = "United States",

note = "1st International Conference on Quantitative Evaluation of Systems, QEST 2004, QEST ; Conference date: 27-09-2004 Through 30-09-2004",

url = "http://www.qest.org/qest2004/",

}

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, 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.1348013

Synthesis and stochastic assessment of schedules for lacquer production. / Bohnenkamp, H.C.; Hermanns, H.; Klaren, J. et al.
First International Conference on Quantitative Evaluation of Systems (QEST 2004). Los Alamitos, California: IEEE, 2004. p. 28-37.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 - Conference code: 1

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

U2 - 10.1109/QEST.2004.1348013

DO - 10.1109/QEST.2004.1348013

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

CY - Los Alamitos, California

T2 - 1st International Conference on Quantitative Evaluation of Systems, QEST 2004

Y2 - 27 September 2004 through 30 September 2004

ER -

Synthesis and stochastic assessment of schedules for lacquer production

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this