Publications

Peer Reviewed

[PBWS17] Guillaume Prevost, Jan Olaf Blech, Keith Foster, Heinrich W. Schmidt. An Architecture for Visualization of Industrial Automation Data. Evaluation of Novel Approaches to Software Engineering (ENASE), ISBN: 978-989-758-250-9, pages 38 – 46, DOI:10.5220/0006289700380046, ScitePress, 2017. [link] [.pdf]

[ASB17] Nasser Alzahrani, Maria Spichkova, Jan Olaf Blech. From Temporal Models to Property-based Testing. Evaluation of Novel Approaches to Software Engineering, 2017.

[STHB17] Alexander Svae, Amir Taherkordi, Peter Herrmann, and Jan Olaf Blech. Self-Adaptive Control in Cyber-Physical Systems: The Autonomous Train Experiment. 32nd ACM Symposium on Applied Computing (ACM SAC) – Cyber-Physical Systems (CPS) Track, Marrakesh, Morocco, April 2017. accepted

[Ble17] Jan Olaf Blech. Behavioral Types for Component-based Software Systems. Australasian Computer Science Week, ACM, 2017.

[THBF16] Amir Taherkordi, Peter Herrmann, Jan Olaf Blech and Alvaro Fernandez. Service Virtualization for Self-Adaptation in Mobile Cyber-Physical Systems. International Workshop on Management of Service-Oriented Cyber-Physical Systems, Banff, Canada, 2016. accepted

[WZBP16] Monika Wenger, Alois Zoitl, Jan Olaf Blech, Ian Peake. Remote Monitoring Infrastructure for IEC 61499 Based Control Software. 8th International Congress on Ultra Modern Telecommunications and Control Systems, IEEE, 2016.

[BFF+16] Jan Olaf Blech, Lasith Fernando, Keith Foster, Abhilash G and Sudarsan Sd. Spatio-temporal Reasoning and Decision Support for Smart Energy Systems. Emerging Technologies and Factory Automation (ETFA), IEEE, 2016.

[BLP+16] Jan Olaf Blech, Per Lindgren, David Pereira, Valeriy Vyatkin and Alois Zoitl. A Comparison of Formal Verification Approaches for IEC 61499. Emerging Technologies and Factory Automation (ETFA), IEEE, 2016.

[PBS16] Ian Peake, Jan Olaf Blech and Matthew Schembri. A Software Framework for Aug-
mented Reality-based Support of Industrial Operations. Emerging Technologies and Factory Automation (ETFA), IEEE, 2016. 

[HOS] S. Hordvik, K. Øseth, H. H. Svendsen, J. O. Blech, P. Herrmann. Model-based Engineer- ing and Spatiotemporal Analysis of Transport Systems. ENASE (Selected Papers) , Springer. to appear

[HB16] Peter Herrmann, Jan Olaf Blech. Formal Model-based Development in Industrial Automation with Reactive Blocks. Workshop on Human-Oriented Formal Methods, 2016

[ASB16] Nasser Alzahrani, Maria Spichkova, Jan Olaf Blech. Spatio-temporal Models for Formal Analysis and Property-based Testing. Workshop on Human-Oriented Formal Methods, 2016.

[PBW+16] Ian D. Peake, Jan Olaf Blech, Edward Watkins, Stefan Greuter, Heinz W. Schmidt. The Virtual Experiences Portals – A Reconfigurable Platform for Immersive Visualization. 3rd International Conference on Augmented Reality, Virtual Reality and Computer Graphics (SALENTO AVR 2016), Springer, 2016. [link]

[OBH16] Magnus Oplenskedal, Jan Olaf Blech, Peter Herrmann. Model-based Development of a Controller and Simulator for a Mobile Robot. ICT International Student Project Conference, IEEE, 2016. [link]

[HOBH16] Simon Hordvik, Kristoffer Øseth, Jan Olaf Blech, Peter Herrmann. A Methodology for Model-based Development and Safety Analysis of Transport Systems. Evaluation of Novel Approaches to Software Engineering, 2016. [link]

[HSSB16] Peter Herrmann, Alexander Svae, Henrik Heggelund Svendsen, Jan Olaf Blech. Collaborative Model-based Development of a Remote Train Monitoring System. Evaluation of Novel Approaches to Software Engineering, COLAFORM Track, 2016. [link]

[HBPT16] James Harland, Jan Olaf Blech, Ian Peake, Luke Trodd. Formal Behavioural Models to Facilitate Distributed Development and Commissioning in Industrial Automation.  Evaluation of Novel Approaches to Software Engineering (ENASE), COLAFORM Track, ISBN 978-989-758-189-2, pages 363-369, ScitePress, 2016. DOI: 10.5220/0005928303630369.  [link] [.pdf]

[FDB+15] Borja Fernández Adiego, Dániel Darvas, Enrique Blanco Viñuela, Jean-Charles Tournier, Simon Bliudze, Jan Olaf Blech, and Víctor Manuel González Suárez. Applying Model Checking to Industrial-Sized PLC Programs. IEEE Transactions on Industrial Informatics, Vol. 11, No. 6, December 2015. [link]

[BSPS15] Jan Olaf Blech, Maria Spichkova, Ian Peake, Heinz W. Schmidt.
Visualization, Simulation and Validation for Cyber-Virtual Systems. Volume 551 of the series Communications in Computer and Information Science, pp. 140-154, Springer 2015. [link]

[ABGS15] Khandakar Ahmed, Jan Olaf Blech, Mark Gregory and Heinz Schmidt. Software Defined Networking for Communication and Control of Cyber-physical Systems. International Workshop on Internet of Things Technologies, IEEE, 2015. [link]

[WZB+15] Monika Wenger, Alois Zoitl, Jan Olaf Blech, Ian Peake, Lasith Fernando. Cloud Based Monitoring of Timed Events for Industrial Automation. Automated Testing of Cyber-Physical Systems in the Cloud, IEEE, 2015. [link]

[PVB+15] Ian D. Peake, Abhijay Vuyyuru, Jan Olaf Blech, Nicolas Vergnaud, Lasith Fernando. Cloud-based Analysis and Control for Robots in Industrial Automation.  Automated Testing of Cyber-Physical Systems in the Cloud, IEEE, 2015. [link]

[BH15a] Jan Olaf Blech and Peter Herrmann. Behavioral Types for Space-aware Systems. Model-based Architecting of Cyber-Physical and Embedded Systems. CEUR proceedings, vol. 1508, 2015. [link]

[BPGR15] Jan Olaf Blech, Ian Peake, Gwyllim Jahn and Roland Snooks. A Software Platform for Architectral Robots. Proceedings of the Australasian Software Engineering Conference (ASWEC), Adelaide, to appear, September, 2015. [link]

[BH15] Jan Olaf Blech, Peter Herrmann. Behavioral Types for Component-based Development of Cyber-Physical Systems. Workshop on Human-Oriented Formal Methods, Springer, 2015. [link]

[BPS+15] Jan Olaf Blech, Ian Peake, Heinz Schmidt, Mallikarjun Kande, Akilur Rahman, Srini Ramaswamy, Sudarsan SD, Venkateswaran Narayanan. Efficient Incident Handling in Indus-
trial Automation through Collaborative Engineering. Emerging Technologies and Factory Au-
tomation (ETFA), IEEE, 2015. [link]

[WBZ15] Monika Wenger, Jan Olaf Blech and Alois Zoitl. Behavioral Type-based Monitoring for IEC 61499. Emerging Technologies and Factory Automation (ETFA), IEEE, 2015. [link]

[PBF+2015] Ian Peake, Jan Olaf Blech, Lasith Fernando, Heinz Schmidt, Ravi Sreenivasamurthy and Sudarsan Sd. Visualization Facilities for Distributed and Remote Industrial Automation: VxLab. Emerging Technologies and Factory Automation (ETFA), IEEE, 2015. [link]

[HBHS15] Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Model-based Engineering and Analysis of Space-aware Systems Communicating via IEEE 802.11. CompSac’15, IEEE, 2015. [link]

[BHPS15] Jan Olaf Blech, Peter Herrmann, Ian Peake and Heinz Schmidt. Towards a Model-based Toolchain for Remote Configuration and Maintenance of Space-aware Systems. Evaluation of Novel Approaches to Software Engineering. ISBN 978-989-758-100-7, SciTePress, 2015. [link]

[PBF+15] Ian Peake, Jan Olaf Blech, Lasith Fernando, Divyasheel Sharma, Srini Ramaswamy and Mallikarjun Kande. Analysis of Software Binaries for Reengineering-Driven Product Line Architecture – An Industrial Case Study. 6th Workshop on Formal Methods and Analysis in SPL Engineering, London, UK, April 11, 2015. [.pdf]

[HBFS14] Peter Herrmann, Jan Olaf Blech, Fenglin Han, and Heinz Schmidt. A Model-based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems. Asia-Pacific Services Computing Conference (APSCC), 2014. Published inInternational Journal of Web Services Research (IJWSR) [link]

[BPS+14] Jan Olaf Blech, Ian Peake, Heinz Schmidt, Mallikarjun Kande, Srini Ramaswamy, Sudarsan Sd, Venkateswaran Narayanan. Collaborative Engineering through Integration of Architectural, Social and Spatial Models. Emerging Technologies and Factory Automation (ETFA), IEEE, 2014. [link]

[SBHS14] Maria Spichkova, Jan Olaf Blech, Peter Herrmann, Heinz Schmidt. Modeling Spatial Aspects of Safety-Critical Systems with FocusST. Model-Driven Engineering, Verification, and Validation (MoDeVVa 2014).

[BSS14] Jan Olaf Blech, Heinz Schmidt, Timos Sellis. Emergency Management Support by Spatial Reasoning. ICSAT Proceedings, ISBN 978-3-319-17999-5, pp 227-232, Springer, 2014. [link]

[BSPS14] Jan Olaf Blech, Maria Spichkova, Ian Peake, Heinz Schmidt. Cyber-Virtual Systems: Simulation, Validation & Visualization. Evaluation of Novel Approaches to Software Engineering. Lisbon, ISBN 978-989-758-030-7, pages 218-225, 2014. DOI: 10.5220/0004952402180225 [link]

[FDB+14] Borja Fernandez Adiego, Daniel Darvas, Enrique Blanco Vinuela, Jean-Charles Tournier, Victor Manuel Gonzalez Suarez, Jan Olaf Blech. Modelling and Formal Verification of Timing Aspects in Large PLC Programs. 19th IFAC World Congress, Cape Town, 2014. [link]

[HBHS14]  Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. Formal Engineering approaches to Software Components and Architectures, 2014. [.pdf]

[Ble13b] Jan Olaf Blech. Ensuring OSGi Component Based Properties at Runtime with Behavioral Types. Model-Driven Engineering, Verification, and Validation, CEUR (ISSN 1613-0073), 2013. [.pdf]

[PBF13] Ian Peake, Jan Olaf Blech, Lasith Fernando. Towards Reconstructing the Architecture of Soft- ware Development Tools by Runtime Analysis. Experiences and Empirical Studies in Software Modelling, CEUR (ISSN 1613-0073), 2013. [.pdf]

[BS2013] Jan Olaf Blech and Heinz Schmidt. Towards Modeling and Checking the Spatial and Interaction Behavior of Widely Distributed Systems. Improving Systems and Software Engineering Conference, Melbourne, 2013. [.pdf]

[Ble13] Jan Olaf Blech. Towards a Framework for Behavioral Specifications of OSGi Components. Formal Engineering approaches to Software Components and Architectures. Electronic Proceedings in Theoretical Computer Science, 2013. [.pdf]

[BFRB12] Jan Olaf Blech, Yliès Falcone, Harald Rueß, Bernhard Schätz. Behavioral Specification based Runtime Monitors for OSGi Services. Leveraging Applicationsof Formal Methods, Verification and Validation (ISoLA), vol. 7609 of LNCS, pp. 405-419, Springer, 2012. [link]

[BFB12] Jan Olaf Blech, Yliès Falcone, and Klaus Becker. Towards Certified Runtime Verification. 14th International Conference on Formal Engineering Methods. Kyoto, Japan, vol. 7635 of LNCS,  pp. 494-509, Springer, 2012. [link]

[BS12] Jan Olaf Blech and Bernhard Schätz. Towards a Formal Foundation of Behavioral Types for UML State-Machines. UML and Formal Methods. Paris, France, ACM SIGSOFT Software Engineering Notes, August 2012. [link]

[BMR12] Jan Olaf Blech,  Dongyue Mou and Daniel Ratiu. Reusing Test-Cases on Different Levels of Abstrac- tion in a Model Based Development Tool. Model-Based Testing, Tallinn, Estonia. Electronic Proceedings in Theoretical Computer Science, pp. 13-27, March 2012. [.pdf]

[HBR+12] Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Static Scheduling of a Time-Triggered Network-on-Chip based on SMT Solving. In Design, Automation and Test in Europe (DATE). Dresden, Germany, IEEE, March 2012. [link]

[Ble11c] Jan Olaf Blech. Probabilistic Compositional Reasoning for Guaranteeing Fault Tolerance Properties. 15th International Conference On Principles Of Distributed Systems, Toulouse, France, vol. 7109 of LNCS, pp. 222-234, Springer, December 2011. [link] [updated report]

[Ble11b] Jan Olaf Blech. A Tool for the Certification of Sequential Function Chart based System Specifications. 6th International Workshop on Systems Software Verification. Nijmegen, ISBN 978-3-939897-36-1, The Netherlands, August 2011. [.pdf]

[BOB11] Jan Olaf Blech and Sidi Ould Biha. Verification of PLC Properties Based on Formal Semantics in Coq. 9th International Conference on Software Engineering and Formal Methods (SEFM), Montevideo, Uruguay, vol. 7041 of LNCS, Springer, 2011. [link]

[HBR+11a] Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Analysis and Optimization of Fault-Tolerant Task Scheduling on Multiprocessor Embedded Systems. In International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS). Embedded System Week. Taipei, Taiwan, ACM, Oct 2011. [link]

[HBR+11] Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Reliability-Aware Design Optimization for Multiprocessor Embedded Systems. 14th Euromicro International Conference on Digital System Design (DSD). Oulu, Finland. Aug 2011. [link]

[BHH11] Jan Olaf Blech, Anton Hattendorf, Jia Huang. An Invariant Preserving Transformation for PLC Models. Model-Based Engineering for Real-Time Embedded Systems Design, IEEE, 2011. [link]

[Ble11] Jan Olaf Blech. Proving the Security of ElGamal Encryption Via Indistinguishability Logic. ACM Symposium On Applied Computing (SAC), 2011. [link]

[BP11] Jan Olaf Blech and Michaël Périn. Generating Invariant-based Certificates for Embedded Systems. ACM Transactions on Embedded Computing Systems (TECS), 2012. [link]

[BG10] Jan Olaf Blech and Benjamin Grégoire. Certifying Compilers Using Higher Order Theorem Provers as Certificate Checkers. Formal Methods in System Design, vol. 38(1). pp. 33-61, Springer-Verlag, 2010. [link]

[BP09] Jan Olaf Blech and Michaël Périn. Certifying Deadlock-freedom for BIP Models. Software and Compilers for Embedded Systems (SCOPES) 2009, ACM, April 2009. [link]

[BNP09] Jan Olaf Blech,Thanh-Hung Nguyen, and Michaël Périn. Invariants and Robustness of BIP Model. International Workshop on Invariant Generation (WING) 2009, March 2009. [link]

[BG09] Jan Olaf Blech and Benjamin Grégoire. Using Checker Predicates in Certifying Code Generation. In Compiler Optimization meets Compiler Verification (COCV 2009), York, UK, March 2009. [.pdf]

[BG08] Jan Olaf Blech and Benjamin Grégoire. Certifying Code Generation with Coq. In Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary, Elsevier ENTCS. April 2008. [.pdf]

[BG08a] Jan Olaf Blech and Benjamin Grégoire. Certifying Code Generation Runs with Coq: A Tool Description. In Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary, Elsevier ENTCS. April 2008. [.pdf]

[BPH07] Jan Olaf Blech and Arnd Poetzsch-Heffter. A certifying code generation phase. In Compiler Optimization meets Compiler Verification (COCV 2007), Braga, Portugal, Elsevier ENTCS. March 2007. [.pdf]

[BSPH07b] Jan Olaf Blech, Ina Schaefer, and Arnd Poetzsch-Heffter. Translation validation for system abstractions. In Runtime Verification (RV’07), Vancouver, Canada, volume 4839 of LNCS. Springer-Verlag, March 2007. [.pdf]

[GB06] Sabine Glesner and Jan Olaf Blech. Coalgebraic semantics for component systems. Springer Verlag, May 2006. Architecting Systems with Trustworthy Components, Lecture Notes in Computer Science, Vol. 3938. [link]

[GLB06] Sabine Glesner, Johannes Leitner, and Jan Olaf Blech. Coinductive verification of program optimizations using similarity relations. In Compiler Optimizations meets Compiler Verification (COCV 2006), Vienna, Austria. Elsevier ENTCS, April 2006. [.pdf]

[BGG05] Jan Olaf Blech, Lars Gesellensetter, and Sabine Glesner. Formal Verification of Dead Code Elimination in Isabelle/HOL. In Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods, pages 200–209. IEEE, IEEE Computer Society Press, September 2005. [.pdf]

[BGL05] Jan Olaf Blech, Sabine Glesner, and Johannes Leitner. Formal Verification of Java Code Generation from UML Models. Proceedings of the 3rd International Fujaba Days 2005: MDD in Practice, 2005. [.pdf]

[BGLM05] Jan Olaf Blech, Sabine Glesner, Johannes Leitner, and Steffen Mülling. Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. In Compiler Optimization meets Compiler Verification, Edinburgh, UK, Elsevier ENTCS, April 2005. [.pdf]

[BG04] Jan Olaf Blech and Sabine Glesner. A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. In Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft für Informatik. Lecture Notes in Informatics, September 2004. [.pdf]

[GB03] Sabine Glesner and Jan Olaf Blech. Classifying and formally verifying integer constant folding. Compiler Optimization meets Compiler Verification (COCV 2003), Warsaw, Poland, Elsevier ENTCS, April 2003. [.pdf]

Reports and Other

[FB16a] Keith Foster, Jan Olaf Blech, Guillaume Prevost. Towards the Formalization of a Factory Demonstrator in BeSpaceD. http://arxiv.org/abs/1612.05316. arXiv.org, 2016.[link]

[FB16] Keith Foster, Jan Olaf Blech. Example Data Sets and Collections for BeSpaceD Ex-
plained. http://arxiv.org/abs/1608.00433. arXiv.org, 2016. [link]

[BF16] Jan Olaf Blech, Keith Foster. Operators for Space and Time in BeSpaceD. http://arxiv.org/abs/1602.08809. arXiv.org, 2016. [link]

[Ble15] Jan Olaf Blech. An Example for BeSpaceD and its Use for Decision Support in Industrial Automation. http://arxiv.org/abs/1512.04656. arXiv.org, 2015. [link]

[PBT+15] Ian Peake, Jan Olaf Blech, Ian Thomas, Nicholas May, Heinz Schmidt, Lasith Fer-
nando, Ravi Sreenivas. The Virtual Experiences Lab a platform for global collaborative en-
gineering and beyond. eResearch Australasia, Brisbane, 2015. Extended Abstract. [link]

[FAD+14] B. Fernandez Adiego, D. Darvas, J-C. Tournier, E. Blanco Vinuela, J. O. Blech, V. Gonzalez Suarez. Automated Generation of Formal Models from ST Control Programs for Verification Purposes. CERN-ACC-NOTE-2014-0037, CERN, Geneva, 2014. [.pdf]

[BS14] Jan Olaf Blech, Heinz Schmidt. BeSpaceD: Towards a Tool Framework and Methodology for the Specification and Verification of Spatial Behavior of Distributed Software Component Systems, http://arxiv.org/abs/1404.3537. arXiv.org, 2014. [.pdf]

[BRS13] J. O. Blech, H. Rueß, B. Schätz. On Behavioral Types for OSGi: From Theory to Implementation. http://arxiv.org/abs/1306.6115. arXiv.org, 2013. [.pdf]

[Ble13a] J.O.Blech and S. Ould Biha: On Formal Reasoning on the Semantics of PLC using Coq. http://arxiv.org/abs/arXiv:1301.3047. arXiv.org 2013. [.pdf]

[Ble12a] J. O. Blech. Towards a Formalization of the OSGi Component Framework. http://arxiv.org/abs/1208.2563v1. arXiv.org 2012. [.pdf]

[Ble12] J. O. Blech. On Compositional Reasoning for Guaranteeing Probabilistic Properties. http://arxiv.org/abs/1203.0415. arXiv.org 2012. [.pdf]

[BBN11] J. O. Blech, B. Boyer, T-H. Nguyen. On the Simulation of Time-Triggered Systems on a Chip with BIP. http://arxiv.org/abs/1109.5505, 2011. [.pdf]

[Ble11a] J. O. Blech. A Tool for the Certification of PLCs based on a Coq Semantics for Sequential Function Charts. http://arxiv.org/abs/1102.3529, 2011. [.pdf]

[BHH10] J. O. Blech, A. Hattendorf, J. Huang. Towards a Property Preserving Transformation from IEC 61131-3 to BIP.http://arxiv.org/abs/1009.0817, 2010. [.pdf]

[Ble09] J. O. Blech. Certifying System Translations Using Higher Order Theorem Provers. PhD- Thesis, ISBN 3832522115, Logos-Verlag, Berlin, 2009. [link]

[BP08] J. O. Blech and M. Périn. Towards Certifying Deadlock-freedom of BIP Models. Technical Report TR-2008-1, Verimag, September 2008. [.pdf]

[BP08a] J. O. Blech and M. Périn. On Certificate Generation and Checking for Deadlock-freedom of BIP Models. Technical Report TR-2008-19, Verimag, December 2008. [.pdf]

[Ble07] J. O. Blech. On certifying code generation. Technical Report 366/07, University of Kaiserslautern, November 2007. [.pdf]

[BSPH07a] J. O. Blech, I. Schaefer, and A. Poetzsch-Heffter. On translation validation for system abstractions. Technical Report 361/07, University of Kaiserslautern, July 2007. [.pdf]

[GBPH06] M. J. Gawkowski, J. O. Blech, and A. Poetzsch-Heffter. Certifying Compilers based on Formal Translation Contracts. Technical Report 355-06, University of Kaiserslautern, November 2006. [.pdf]

[Ble04] J. O. Blech. Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL. Universität Karlsruhe, March 2004. (Diplomarbeit) [.pdf]

[Ble03] J. O. Blech. Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern. Universität Karlsruhe, Mai 2003. (Studienarbeit) [.pdf]

Leave a Reply