Dr. rer. nat. Dimitri Bohlender

Kontakt

Wissenschaftlicher Mitarbeiter

Tel. +49 241 80 21174
Fax +49 241 80 22150


Adresse: Ahornstr. 55, 52074 Aachen, Germany
Büro: Raum 2302 (Gebäude H, 3.OG)

Email: bohlender[at]embedded[dot]rwth-aachen[dot]de
Web: bohlender.pro

Offene Abschlussarbeiten

Aktuell liegen keine ausformulierten, offenen Abschlussarbeiten vor. Bei Interesse an formalen Methoden können wir aber zusammen geeignete Themen für Bachelor- und Masterarbeiten ausarbeiten. Eigene Vorschläge sind ebenfalls möglich.

Lehre

Publikationen


Publikations-Export
[Boh21]
Bohlender, D., "Symbolic methods for formal verification of industrial control software", PhD Thesis, Aachen, 2021.

Symbolic methods for formal verification of industrial control software

Bibtex entry :

@phdthesis {  Boh21,
	author = { Bohlender, Dimitri },
	othercontributors = { Kowalewski, Stefan and Hermanns, Holger },
	title = { Symbolic methods for formal verification of industrial
		control software },
	publisher = { RWTH Aachen University },
	school = { RWTH Aachen University },
	pages = { 1 Online-Ressource : Illustrationen, Diagramme },
	series = { Aachener Informatik-Berichte },
	year = { 2021 },
	address = { Aachen },
	doi = { 10.18154/RWTH-2021-10633 },
	typ = { PUB:(DE-HGF)11 },
	reportid = { RWTH-2021-10633 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/835546/files/835546.pdf },
}
[GSB+20]
PDFBIB
Grochowski, M., Simon, H., Bohlender, D., Kowalewski, S., Löcklin, A., Müller, T., Jazdi, N., Zeller, A., and Weyrich, M., "Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion", Automatisierungstechnik, vol. 68, iss. 1, pp. 3-14, 2020

Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion

Bibtex entry :

@article {  GSB+20,
	author = { Grochowski, Marco and Simon, Hendrik and Bohlender, Dimitri
		and Kowalewski, Stefan and L{\"o}cklin, Andreas and
		M{\"u}ller, Timo and Jazdi, Nasser and Zeller, Andreas and
		Weyrich, Michael },
	title = { Formale Methoden f{\"u}r rekonfigurierbare cyber-physische
		Systeme in der Produktion },
	journal = { Automatisierungstechnik },
	publisher = { De Gruyter },
	pages = { 3-14 },
	volume = { 68 },
	number = { 1 },
	year = { 2020 },
	address = { Berlin },
	issn = { 2196-677X },
	doi = { 10.1515/auto-2019-0115 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12214 },
	cin = { 122810 / 120000 },
}
[BCK+19]
Bohlender, D., Chiyah Garcia, F. J., Köhl, M., Menghi, C., and Wortmann, A., "On Explainability and its Characterization", , pp. 4-7, 2019

On Explainability and its Characterization

Bibtex entry :

@article {  BCK+19,
	author = { Bohlender, Dimitri and Chiyah Garcia, Francisco J. and
		K{\"o}hl, Maximilian and Menghi, Claudio and Wortmann,
		Andreas },
	title = { On Explainability and its Characterization },
	pages = { 4-7 },
	year = { 2019 },
	organization = { GI Dagstuhl Seminar 19023 on Explainable Software for
		Cyber-Physical Systems, Dagstuhl (Germany), 2019-01-06 -
		2019-01-11 },
	doi = { 10.18154/RWTH-2020-01625 },
	typ = { PUB:(DE-HGF)25 },
	reportid = { RWTH-2020-01625 },
	cin = { 122810 / 120000 / 121510 },
	url = { https://arxiv.org/pdf/1904.11851.pdf#page=9 },
}
[BK19]
Bohlender, D. and Kowalewski, S., "Leveraging Horn clause solving for compositional verification of PLC software", Discrete event dynamic systems, vol. 30, pp. 1-24, 2019

Leveraging Horn clause solving for compositional verification of PLC software

Bibtex entry :

@article {  BK19,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Leveraging Horn clause solving for compositional
		verification of PLC software },
	journal = { Discrete event dynamic systems },
	publisher = { Springer Science + Business Media B.V },
	pages = { 1-24 },
	volume = { 30 },
	year = { 2019 },
	address = { Dordrecht [u.a.] },
	issn = { 1573-7594 },
	doi = { 10.1007/s10626-019-00296-8 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12207 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/775404 },
}
[BK19a]
Bohlender, D. and Köhl, M. A., "Towards a Characterization of Explainable Systems", , 2019

Towards a Characterization of Explainable Systems

Bibtex entry :

@article {  BK19a,
	author = { Bohlender, Dimitri and K{\"o}hl, Maximilian A. },
	title = { Towards a Characterization of Explainable Systems },
	year = { 2019 },
	typ = { PUB:(DE-HGF)25 },
	reportid = { RWTH-2020-01624 },
	cin = { 122810 / 120000 },
	url = { https://www.semanticscholar.org/paper/Towards-a-Characterization-of-Explainable-Systems-Bohlender-K%C3%B6hl/b3516a71fed895a1a88b7d9842eca41c0fb48b7d },
}
[KBL+19]
Köhl, M. A., Baum, K., Langer, M., Oster, D., Speith, T., and Bohlender, D., "Explainability as a Non-Functional Requirement", in Proc. 2019 IEEE 27th International Requirements Engineering Conference : 23-27 September 2019, Jeju Island, South Korea : proceedings / editors: Daniela Damian and Anna Perini (Program Chairs), Seok-Won Lee (General Chair), Piscataway, JN, 2019, IEEE, pp. 363-368.

Explainability as a Non-Functional Requirement

Bibtex entry :

@inproceedings {  KBL+19,
	author = { K{\"o}hl, Maximilian A. and Baum, Kevin and Langer, Markus
		and Oster, Daniel and Speith, Timo and Bohlender, Dimitri },
	title = { Explainability as a Non-Functional Requirement },
	booktitle = { 2019 IEEE 27th International Requirements Engineering
		Conference : 23-27 September 2019, Jeju Island, South Korea
		: proceedings / editors: Daniela Damian and Anna Perini
		(Program Chairs), Seok-Won Lee (General Chair) },
	publisher = { IEEE },
	pages = { 363-368 },
	year = { 2019 },
	address = { Piscataway, JN },
	organization = { IEEE 27. International Requirements Engineering Conference,
		Jeju Island (South Korea), 2019-09-23 - 2019-09-27 },
	doi = { 10.1109/RE.2019.00046 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2019-12206 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/775403 },
}
[BHK18]
Bohlender, D., Hamm, D., and Kowalewski, S., "Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding", in Proc. Applied computing 2018 : the 33rd Annual ACM Symposium on Applied Computing : Pau, France, April 9-13, 2018 / sponsored by: ACM Special Interest Group on Applied Computing ; conference chairs: Hisham M. Haddad (Kennesaw State University, USA), Roger L. Wainwright (University of Tulsa, USA), Richard Chbeir (University of Pau & Pays Adour, France), New York, NY, 2018, ACM, pp. 1891-1898.

Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding

Bibtex entry :

@inproceedings {  BHK18,
	author = { Bohlender, Dimitri and Hamm, Daniel and Kowalewski, Stefan },
	title = { Cycle-Bounded Model Checking of PLC Software via Dynamic
		Large-Block Encoding },
	booktitle = { Applied computing 2018 : the 33rd Annual ACM Symposium on
		Applied Computing : Pau, France, April 9-13, 2018 /
		sponsored by: ACM Special Interest Group on Applied
		Computing ; conference chairs: Hisham M. Haddad (Kennesaw
		State University, USA), Roger L. Wainwright (University of
		Tulsa, USA), Richard Chbeir (University of Pau & Pays Adour,
		France) },
	publisher = { ACM },
	pages = { 1891-1898 },
	year = { 2018 },
	address = { New York, NY },
	organization = { 33. ACM Symposium on Applied Computing, Pau (France),
		2018-04-09 - 2018-04-13 },
	doi = { 10.1145/3167132.3167334 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-231950 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752221 },
}
[BK18]
Bohlender, D. and Kowalewski, S., "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", IFAC-PapersOnLine, vol. 51, iss. 7, pp. 428-433, 2018

Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction

Bibtex entry :

@article {  BK18,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Compositional Verification of PLC Software using Horn
		Clauses and Mode Abstraction },
	journal = { IFAC-PapersOnLine },
	pages = { 428-433 },
	volume = { 51 },
	number = { 7 },
	year = { 2018 },
	address = { Laxenburg },
	issn = { 2405-8963 },
	organization = { 14. IFAC International Workshop on Discrete Event Systems,
		Castellammare di Stabia (Italy), 2018-05-30 - 2018-06-01 },
	doi = { 10.1016/j.ifacol.2018.06.336 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2018-227071 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/730763 },
}
[BK18a]
Bohlender, D. and Kowalewski, S., "Design and Verification of Restart-Robust Industrial Control Software", in Proc. Integrated formal methods : 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018 : proceedings / Carlo A. Furia, Kirsten Winter (eds.), Cham, 2018 in Lecture notes in computer science, Springer, pp. 47-68.

Design and Verification of Restart-Robust Industrial Control Software

Bibtex entry :

@inproceedings {  BK18a,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Design and Verification of Restart-Robust Industrial Control
		Software },
	booktitle = { Integrated formal methods : 14th International Conference,
		IFM 2018, Maynooth, Ireland, September 5-7, 2018 :
		proceedings / Carlo A. Furia, Kirsten Winter (eds.) },
	publisher = { Springer },
	pages = { 47-68 },
	series = { Lecture notes in computer science },
	year = { 2018 },
	address = { Cham },
	organization = { 14. International Conference on Integrated Formal Methods,
		Maynooth (Ireland), 2018-09-05 - 2018-09-07 },
	doi = { 10.1007/978-3-319-98938-9_4 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-231948 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752219 },
}
[UVS+17]
Ulewicz, S., Vogel-Heuser, B., Simon, H., Bohlender, D., Obster, M., and Kowalewski, S., "A priori test coverage estimation for automated production systems : Using generated behavior models for coverage calculation", in Proc. 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation : September 12-15, 2017, Limassol, Cyprus / ABB, IEEE, IES, University of Cyprus, Piscataway, NJ, 2017, IEEE, p. 4.

A priori test coverage estimation for automated production systems : Using generated behavior models for coverage calculation

Bibtex entry :

@inproceedings {  UVS+17,
	author = { Ulewicz, Sebastian and Vogel-Heuser, Birgit and Simon,
		Hendrik and Bohlender, Dimitri and Obster, Mathias and
		Kowalewski, Stefan },
	title = { A priori test coverage estimation for automated production
		systems : Using generated behavior models for coverage
		calculation },
	booktitle = { 2017 22nd IEEE International Conference on Emerging
		Technologies and Factory Automation : September 12-15, 2017,
		Limassol, Cyprus / ABB, IEEE, IES, University of Cyprus },
	publisher = { IEEE },
	pages = { 4 Seiten },
	year = { 2017 },
	address = { Piscataway, NJ },
	organization = { 22. IEEE International Conference on Emerging Technologies
		and Factory Automation, Limassol (Cyprus), 2017-09-12 -
		2017-09-15 },
	doi = { 10.1109/ETFA.2017.8247704 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2018-223451 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/722217 },
}
[BSF+16]
Bohlender, D., Simon, H., Friedrich, N., Kowalewski, S., and Hauck-Stattelmann, S., "Concolic test generation for PLC programs using coverage metrics", in Proc. 2016 13th International Workshop on Discrete Event Systems (WODES) : May 30-June 1, 2016, Xi'an, China / edited by Christos G. Cassandras, Alessandro Giua, Zhiwu Li ; sponsored by IEEE - Control Systems Society, Piscataway, NJ, 2016, IEEE, pp. 432-437.

Concolic test generation for PLC programs using coverage metrics

Bibtex entry :

@inproceedings {  BSF+16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Friedrich, Nico
		and Kowalewski, Stefan and Hauck-Stattelmann, Stefan },
	title = { Concolic test generation for PLC programs using coverage
		metrics },
	booktitle = { 2016 13th International Workshop on Discrete Event Systems
		(WODES) : May 30-June 1, 2016, Xi'an, China / edited by
		Christos G. Cassandras, Alessandro Giua, Zhiwu Li ;
		sponsored by IEEE - Control Systems Society },
	publisher = { IEEE },
	pages = { 432-437 },
	year = { 2016 },
	address = { Piscataway, NJ },
	organization = { 13. International Workshop on Discrete Event Systems, Xi'an
		(Peoples R China), 2016-05-30 - 2016-06-01 },
	doi = { 10.1109/WODES.2016.7497884 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2016-11193 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/679431 },
}
[BSK+16]
Bohlender, D., Simon, H., Kowalewski, S., and Hauck-Stattelmann, S., "Symbolische Ausführung zum Testen von SPS-Programmen", in Proc. Automation 2016 : secure & reliable in the digital world : 17. Branchentreff der Mess- und Automatisierungstechnik : Baden-Baden, 07. und 08. Juni 2016 / VDI/VDE Mess- und Automatisierungstechnik, Düsseldorf, 2016 in VDI-Berichte, VDI Verlag GmbH, pp. 13-14.

Symbolische Ausführung zum Testen von SPS-Programmen

Bibtex entry :

@inproceedings {  BSK+16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, S. },
	title = { Symbolische Ausf{\"u}hrung zum Testen von SPS-Programmen },
	booktitle = { Automation 2016 : secure & reliable in the digital world :
		17. Branchentreff der Mess- und Automatisierungstechnik :
		Baden-Baden, 07. und 08. Juni 2016 / VDI/VDE Mess- und
		Automatisierungstechnik },
	publisher = { VDI Verlag GmbH },
	pages = { 13-14 },
	series = { VDI-Berichte },
	year = { 2016 },
	address = { D{\"u}sseldorf },
	organization = { 17. Branchentreff der Mess- und Automatisierungstechnik,
		Baden-Baden (Germany), 2016-06-07 - 2016-06-08 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-2016-12035 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/680852 },
}
[BSK16]
Bohlender, D., Simon, H., and Kowalewski, S., "Symbolic verification of PLC safety-applications based on PLCopen automata", in Proc. MBMV 2016 : 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" : Albert-Ludwigs-Universität Freiburg im Breisgau 1.–2. März 2016 / Ralf Wimmer (Herausgeber), Freiburg im Breisgau, 2016, Albert-Ludwigs-Universität, pp. 33-45.

Symbolic verification of PLC safety-applications based on PLCopen automata

Bibtex entry :

@inproceedings {  BSK16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan },
	title = { Symbolic verification of PLC safety-applications based on
		PLCopen automata },
	booktitle = { MBMV 2016 : 19. GI/ITG/GMM-Workshop "Methoden und
		Beschreibungsprachen zur Modellierung und Verifikation von
		Schaltungen und Systemen" : Albert-Ludwigs-Universit{\"a}t
		Freiburg im Breisgau 1.–2. M{\"a}rz 2016 / Ralf Wimmer
		(Herausgeber) },
	publisher = { Albert-Ludwigs-Universit{\"a}t },
	pages = { 33-45 },
	year = { 2016 },
	address = { Freiburg im Breisgau },
	organization = { 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen
		zur Modellierung und Verifikation von Schaltungen und
		Systemen", Freiburg im Breisgau (Germany), 2016-03-01 -
		2016-03-02 },
	doi = { 10.6094/UNIFR/10636 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-207902 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/573821/files/573821.pdf },
}
[BBJKNN14]
PDFBIB
Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V. Y., and Noll, T., "A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models", in Proc. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part {II}, 2014, IEEE, pp. 177-192.

A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models

Bibtex entry :

@inproceedings { BBJKNN14,
	author = { Dimitri Bohlender and Harold Bruintjes and Sebastian Junges
		and Jens Katelaan and Viet Yen Nguyen and Thomas Noll },
	title = { A Review of Statistical Model Checking Pitfalls on Real-Time
		Stochastic Models },
	booktitle = { Leveraging Applications of Formal Methods, Verification and
		Validation. Specialized Techniques and Applications - 6th
		International Symposium, ISoLA 2014, Imperial, Corfu,
		Greece, October 8-11, 2014, Proceedings, Part {II} },
	pages = { 177--192 },
	publisher = { IEEE },
	publishedas = { Druck Online },
	isbn = { 978-3-662-45231-8 },
	language = { eng },
	year = { 2014 },
	timestamp = { Mon, 29 Sep 2014 11:09:02 +0200 },
	i11key = { conference },
	for_reporting_period = { 2014 },
}
[BBK13]
Biallas, S., Bohlender, D., and Kowalewski, S., "Boolean and Modular Abstractions for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems : DCDS13. - Vol. 4, P. 1, Laxenburg, 2013, IFAC, pp. 97-102.

Boolean and Modular Abstractions for Programmable Logic Controllers

Bibtex entry :

@inproceedings {  BBK13,
	author = { Biallas, Sebastian and Bohlender, Dimitri and Kowalewski,
		Stefan },
	title = { Boolean and Modular Abstractions for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems : DCDS13. - Vol. 4,
		P. 1 },
	publisher = { IFAC },
	pages = { 97-102 },
	year = { 2013 },
	address = { Laxenburg },
	organization = { Dependable Control of Discrete Systems },
	doi = { 10.3182/20130904-3-UK-4041.00011 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203363 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/225788 },
}
Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland