Room: G29, R402
Phone: +49 391 67 52705
Marco Filax received a BSc and an MSc in Computational Visualistics at the Otto von Guericke University. Marco is a research assistant at the Chair of Software Engineering since 2014. His research interests include but are not limited to pattern recognition, computer vision, pervasive cameras, formal verification techniques, and requirement analysis.
Marco Filax
Publications
2020 |
Ataide, Elmer; Fritzsche, Holger; Filax, Marco; Chittamuri, Dinesh; Potluri, Lakshmi; Friebe, Michael ENT Endoscopic Surgery and Mixed Reality: Application Development and Integration Buchkapitel mit eigenem Titel Biomedical and Clinical Engineering for Healthcare Advancement, S. 17-29, IGI Global, 2020. @incollection{Ataide20, title = {ENT Endoscopic Surgery and Mixed Reality: Application Development and Integration}, author = {Elmer Ataide and Holger Fritzsche and Marco Filax and Dinesh Chittamuri and Lakshmi Potluri and Michael Friebe}, url = {https://www.igi-global.com/gateway/chapter/239074}, year = {2020}, date = {2020-01-01}, booktitle = {Biomedical and Clinical Engineering for Healthcare Advancement}, pages = {17-29}, publisher = {IGI Global}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } |
2019 |
Gonschorek, Tim; Bergt, Philipp; Filax, Marco; Ortmeier, Frank Integrating Safety Design Artifacts into System Development Models Using SafeDeML Inproceedings Papadopoulos, Yiannis; Aslansefat, Koorosh; Katsaros, Panagiotis; Bozzano, Marco (Hrsg.): Model-Based Safety and Assessment, S. 93–106, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-32872-6. @inproceedings{10.1007/978-3-030-32872-6_7, title = {Integrating Safety Design Artifacts into System Development Models Using SafeDeML}, author = {Tim Gonschorek and Philipp Bergt and Marco Filax and Frank Ortmeier}, editor = {Yiannis Papadopoulos and Koorosh Aslansefat and Panagiotis Katsaros and Marco Bozzano}, url = {https://link.springer.com/chapter/10.1007/978-3-030-32872-6_7}, doi = {10.1007/978-3-030-32872-6_7}, isbn = {978-3-030-32872-6}, year = {2019}, date = {2019-09-18}, booktitle = {Model-Based Safety and Assessment}, pages = {93--106}, publisher = {Springer International Publishing}, address = {Cham}, abstract = {Applying a safety artifact language as Safety Design Modeling Language SafeDeML integrates the generation of the safety design into the system modeling stage -- directly within the system architecture. In this paper, we present a modeling process and a prototype for the CASE tool Enterprise Architect for SafeDeML. The goal is to support the system designer in developing a standard (in this paper Iso 26262) conform system and safety design containing all relevant safety artifact within one model. Such integration offers several modeling guarantees like consistency checks or computation of coverage and fault metrics. Since all relevant information and artifacts are contained within the model, SafeDeML and the prototype can help to decrease the effect of structural faults during the safety design and further supports the safety assessment. To give an idea to the reader of the complexity of the approach's application, we present an exemplary implementation of the safety design for a brake light system, a real case-study from the Iso 26262 context.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Applying a safety artifact language as Safety Design Modeling Language SafeDeML integrates the generation of the safety design into the system modeling stage -- directly within the system architecture. In this paper, we present a modeling process and a prototype for the CASE tool Enterprise Architect for SafeDeML. The goal is to support the system designer in developing a standard (in this paper Iso 26262) conform system and safety design containing all relevant safety artifact within one model. Such integration offers several modeling guarantees like consistency checks or computation of coverage and fault metrics. Since all relevant information and artifacts are contained within the model, SafeDeML and the prototype can help to decrease the effect of structural faults during the safety design and further supports the safety assessment. To give an idea to the reader of the complexity of the approach's application, we present an exemplary implementation of the safety design for a brake light system, a real case-study from the Iso 26262 context. |
Gonschorek, Tim; Bergt, Philipp; Filax, Marco; Ortmeier, Frank; von Hoyningen-Hüne, Jan; Piper, Thorsten SafeDeML: On Integrating the Safety Design into the System Model Inproceedings Romanovsky, Alexander; Troubitsyna, Elena; Bitsch, Friedemann (Hrsg.): Computer Safety, Reliability, and Security, S. 271–285, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-26601-1. @inproceedings{10.1007/978-3-030-26601-1_19, title = {SafeDeML: On Integrating the Safety Design into the System Model}, author = {Tim Gonschorek and Philipp Bergt and Marco Filax and Frank Ortmeier and Jan von Hoyningen-H\"{u}ne and Thorsten Piper}, editor = {Alexander Romanovsky and Elena Troubitsyna and Friedemann Bitsch}, url = {https://link.springer.com/chapter/10.1007/978-3-030-26601-1_19}, doi = {10.1007/978-3-030-26601-1_19}, isbn = {978-3-030-26601-1}, year = {2019}, date = {2019-09-18}, booktitle = {Computer Safety, Reliability, and Security}, pages = {271--285}, publisher = {Springer International Publishing}, address = {Cham}, abstract = {The safety design definition of a safety critical system is a complex task. On the one hand, the system designer must ensure that he addressed all potentially hazardous harwdware faults. This is often defined not(!) in the model but within extra documents (e.g., Excel sheets). On the other hand, all defined safety mechanisms must be transformed back into the system model. We think an improvement for the designer would be given by a modeling extension integrating relevant safety design artifacts into the normal design work-flow and supporting the safety design development directly from within the model.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The safety design definition of a safety critical system is a complex task. On the one hand, the system designer must ensure that he addressed all potentially hazardous harwdware faults. This is often defined not(!) in the model but within extra documents (e.g., Excel sheets). On the other hand, all defined safety mechanisms must be transformed back into the system model. We think an improvement for the designer would be given by a modeling extension integrating relevant safety design artifacts into the normal design work-flow and supporting the safety design development directly from within the model. |
Filax, Marco; Gonschorek, Tim; Ortmeier, Frank Data for Image Recognition Tasks: An Efficient Tool for Fine-Grained Annotations Inproceedings Proceedings of the 8th International Conference on Pattern Recognition Applications and Methods, 2019. @inproceedings{Filax2019, title = {Data for Image Recognition Tasks: An Efficient Tool for Fine-Grained Annotations}, author = {Marco Filax and Tim Gonschorek and Frank Ortmeier}, url = {https://bitbucket.org/cse_admin/md_groceries}, year = {2019}, date = {2019-02-19}, booktitle = {Proceedings of the 8th International Conference on Pattern Recognition Applications and Methods}, abstract = {Using large datasets is essential for machine learning. In practice, training a machine learning algorithm requires hundreds of samples. Multiple off-the-shelf datasets from the scientific domain exist to benchmark new approaches. However, when machine learning algorithms transit to industry, e.g., for a particular image classification problem, hundreds of specific purpose images are collected and annotated in laborious manual work. In this paper, we present a novel system to decrease the effort of annotating those large image sets. Therefore, we generate 2D bounding boxes from minimal 3D annotations using the known location and orientation of the camera. We annotate a particular object of interest in 3D once and project these annotations on to every frame of a video stream. The proposed approach is designed to work with off-the-shelf hardware. We demonstrate its applicability with an example from the real world. We generated a more extensive dataset than available in other works for a particular industrial use case: fine-grained recognition of items within grocery stores. Further, we make our dataset available to the interested vision community consisting of over 60,000 images. Some images were taken under ideal conditions for training while others were taken with the proposed approach in the wild. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Using large datasets is essential for machine learning. In practice, training a machine learning algorithm requires hundreds of samples. Multiple off-the-shelf datasets from the scientific domain exist to benchmark new approaches. However, when machine learning algorithms transit to industry, e.g., for a particular image classification problem, hundreds of specific purpose images are collected and annotated in laborious manual work. In this paper, we present a novel system to decrease the effort of annotating those large image sets. Therefore, we generate 2D bounding boxes from minimal 3D annotations using the known location and orientation of the camera. We annotate a particular object of interest in 3D once and project these annotations on to every frame of a video stream. The proposed approach is designed to work with off-the-shelf hardware. We demonstrate its applicability with an example from the real world. We generated a more extensive dataset than available in other works for a particular industrial use case: fine-grained recognition of items within grocery stores. Further, we make our dataset available to the interested vision community consisting of over 60,000 images. Some images were taken under ideal conditions for training while others were taken with the proposed approach in the wild. |
2018 |
Gonschorek, Tim; Filax, Marco; Ortmeier, Frank A very first Glance on the Safety Analysis of Self-learning Algorithms for Autonomous Cars Inproceedings Guiochet, Jérémie (Hrsg.): 37th International Conference on Computer Safety, Reliability, & Security. SAFECOMP2018., HAL, 2018. @inproceedings{Gonschorek2018c, title = {A very first Glance on the Safety Analysis of Self-learning Algorithms for Autonomous Cars}, author = {Tim Gonschorek and Marco Filax and Frank Ortmeier}, editor = {J'{e}r'{e}mie Guiochet}, url = {https://hal.archives-ouvertes.fr/hal-01878562v1 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2019/01/fastAbstractGonschorekEtAl_AVery-FirstGlanceOnThe-SafetyAnalysisOfSelf-learningAlgorithmsForAutonomousCars.pdf}, year = {2018}, date = {2018-09-26}, booktitle = {37th International Conference on Computer Safety, Reliability, & Security. SAFECOMP2018.}, publisher = {HAL}, series = {Fast Abstracts}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Kögel, Markus; Andonov, Petar; Filax, Marco; Ortmeier, Frank; Findeisen, Rolf Predictive Tracking Control of a Camera - Head Mounted Display System subject to Communication Constraints Inproceedings 16th European Control Conference (ECC), S. 1035-1041, 2018. @inproceedings{Koegel18, title = {Predictive Tracking Control of a Camera - Head Mounted Display System subject to Communication Constraints}, author = {Markus K\"{o}gel and Petar Andonov and Marco Filax and Frank Ortmeier and Rolf Findeisen}, year = {2018}, date = {2018-06-01}, booktitle = {16th European Control Conference (ECC)}, pages = {1035-1041}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Klockmann, Maximilian; Filax, Marco; Ortmeier, Frank; Reiß, Martin On the Similarities of Fingerprints and Railroad Tracks: Using Minutiae Detection Algorithms to digitize Track Plans. Inproceedings 13th IAPR Workshop on Document Analysis Systems (DAS), 2018. @inproceedings{klock18, title = {On the Similarities of Fingerprints and Railroad Tracks: Using Minutiae Detection Algorithms to digitize Track Plans.}, author = {Maximilian Klockmann and Marco Filax and Frank Ortmeier and Martin Rei{\ss}}, year = {2018}, date = {2018-01-01}, booktitle = {13th IAPR Workshop on Document Analysis Systems (DAS)}, abstract = {The complete track system of Germany covers more than 42.000 kilometers - some built before 1970. As a consequence, technical drawings are typical of manual origin. Newer plans are generated in a computer-aided way but remain drawings in the sense that semantics are not captured in the electronic files themselves. The engineer decides the meaning of a symbol while viewing the document. For project realization (e.g., engineering of some interlocking system), these plans are digitized manually into some machine interpretable format. In this paper, we propose an approach to digitize track layouts (semi-)automatically. We use fingerprint recognition techniques to digitize manually created track plans efficiently. At first, we detect tracks by detecting line endings and bifurcations. Secondly, we eliminate false candidates and irregularities. Finally, we translate the resulting graph into an interchangeable format RailML. We evaluate our method by comparing our results with different track plans. Our results indicate that the proposed method is a promising candidate, reducing the effort of digitization. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The complete track system of Germany covers more than 42.000 kilometers - some built before 1970. As a consequence, technical drawings are typical of manual origin. Newer plans are generated in a computer-aided way but remain drawings in the sense that semantics are not captured in the electronic files themselves. The engineer decides the meaning of a symbol while viewing the document. For project realization (e.g., engineering of some interlocking system), these plans are digitized manually into some machine interpretable format. In this paper, we propose an approach to digitize track layouts (semi-)automatically. We use fingerprint recognition techniques to digitize manually created track plans efficiently. At first, we detect tracks by detecting line endings and bifurcations. Secondly, we eliminate false candidates and irregularities. Finally, we translate the resulting graph into an interchangeable format RailML. We evaluate our method by comparing our results with different track plans. Our results indicate that the proposed method is a promising candidate, reducing the effort of digitization. |
Filax, Marco; Ortmeier, Frank VIOL: Viewpoint Invariant Object Localizator - Viewpoint Invariant Planar Features in Man-Made Environments Inproceedings Conference on Computer Vision, Imaging and Computer Graphics Theory and Applications (VISAPP), S. 581-588, 2018, ISBN: 978-989-758-290-5. @inproceedings{visapp18, title = {VIOL: Viewpoint Invariant Object Localizator - Viewpoint Invariant Planar Features in Man-Made Environments}, author = {Marco Filax and Frank Ortmeier}, doi = {10.5220/0006624005810588}, isbn = {978-989-758-290-5}, year = {2018}, date = {2018-01-01}, booktitle = {Conference on Computer Vision, Imaging and Computer Graphics Theory and Applications (VISAPP)}, pages = {581-588}, abstract = {Object detection is one of the fundamental issues in computer vision. The established methods, rely on different feature descriptors to determine correspondences between significant image points. However, they do not provide reliable results, especially for extreme viewpoint changes. This is because feature descriptors do not adhere to the projective distortion introduced with an extreme viewpoint change. Different approaches have been proposed to lower this hurdle, e.g., by randomly sampling multiple virtual viewpoints. However, these methods are either computationally intensive or impose strong assumptions of the environment. In this paper, we propose an algorithm to detect corresponding quasi-planar objects in man-made environments. We make use of the observation that these environments typically contain rectangular structures. We exploit the information gathered from a depth sensor to detect planar regions. With these, we unwrap the projective distortion, by transforming the planar patch into a fronto-parallel view. We demonstrate the feasibility and capabilities of our approach in a real-world scenario: a supermarket.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Object detection is one of the fundamental issues in computer vision. The established methods, rely on different feature descriptors to determine correspondences between significant image points. However, they do not provide reliable results, especially for extreme viewpoint changes. This is because feature descriptors do not adhere to the projective distortion introduced with an extreme viewpoint change. Different approaches have been proposed to lower this hurdle, e.g., by randomly sampling multiple virtual viewpoints. However, these methods are either computationally intensive or impose strong assumptions of the environment. In this paper, we propose an algorithm to detect corresponding quasi-planar objects in man-made environments. We make use of the observation that these environments typically contain rectangular structures. We exploit the information gathered from a depth sensor to detect planar regions. With these, we unwrap the projective distortion, by transforming the planar patch into a fronto-parallel view. We demonstrate the feasibility and capabilities of our approach in a real-world scenario: a supermarket. |
2017 |
Gonschorek, Tim; Filax, Marco; Ortmeier, Frank Invited Paper: 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017), 2017. @misc{Gonschorek2017b, title = {A Verification Environment for Critical Systems: Integrating Formal Methods into the Safety Development Life-cycle}, author = {Tim Gonschorek and Marco Filax and Frank Ortmeier}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_-VECS_imbsa17_poster.pdf https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_-VECS_imbsa17_poster.pdf}, year = {2017}, date = {2017-09-11}, howpublished = {Invited Paper: 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017)}, keywords = {}, pubstate = {published}, tppubtype = {misc} } |
Filax, Marco; Gonschorek, Tim; Ortmeier, Frank Building Models we can rely on: Requirements Traceability for Model-based Verification Techniques Inproceedings Bozzano M., Papadopoulos Y (Hrsg.): Proceedings of the 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017), S. 3-18, Springer, Cham, 2017, ISBN: 978-3-319-64118-8 . @inproceedings{Filax2017, title = {Building Models we can rely on: Requirements Traceability for Model-based Verification Techniques}, author = {Marco Filax and Tim Gonschorek and Frank Ortmeier}, editor = {Bozzano M., Papadopoulos Y.}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/08/imbsa17_preprint.pdf}, doi = {10.1007/978-3-319-64119-5_1}, isbn = {978-3-319-64118-8 }, year = {2017}, date = {2017-09-11}, booktitle = {Proceedings of the 5th International Symposium on Model-Based Safety and Assessment (IMBSA 2017)}, volume = {10437}, pages = {3-18}, publisher = {Springer, Cham}, series = { Lecture Notes in Computer Science}, abstract = {Proving the safety of a critical system is a complex and complicated task. Model-based formal verification techniques can help to verify a System Requirement Specification (SRS) with respect to normative and safety requirements. Due to an early application of these methods, it is possible to reduce the risk of high costs caused by unexpected, late system adjustments. Nevertheless, they are still rarely used. One reason among others is the lack of an applicable integration method in an existing development process. In this paper, we propose a process to integrate formal model-based verification techniques into the development life-cycle of a safety critical system. The core idea is to systematically refine informal specifications by 1) categorization, 2) structural refinement, 3) expected behavioral refinement, and finally, 4) operational semantics. To support modeling, traceability is upheld through all refinement steps and a number of consistency checks are introduced. The proposed process has been jointly developed with the German Railroad Authority (EBA) and an accredited safety assessor. We implemented an Eclipse-based IDE with connections to requirement and systems engineering tools as well as various verification engines. The applicability of our approach is demonstrated via an industrial-sized case study in the context of the European Train Control System with ETCS Level 1 Full Supervision. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Proving the safety of a critical system is a complex and complicated task. Model-based formal verification techniques can help to verify a System Requirement Specification (SRS) with respect to normative and safety requirements. Due to an early application of these methods, it is possible to reduce the risk of high costs caused by unexpected, late system adjustments. Nevertheless, they are still rarely used. One reason among others is the lack of an applicable integration method in an existing development process. In this paper, we propose a process to integrate formal model-based verification techniques into the development life-cycle of a safety critical system. The core idea is to systematically refine informal specifications by 1) categorization, 2) structural refinement, 3) expected behavioral refinement, and finally, 4) operational semantics. To support modeling, traceability is upheld through all refinement steps and a number of consistency checks are introduced. The proposed process has been jointly developed with the German Railroad Authority (EBA) and an accredited safety assessor. We implemented an Eclipse-based IDE with connections to requirement and systems engineering tools as well as various verification engines. The applicability of our approach is demonstrated via an industrial-sized case study in the context of the European Train Control System with ETCS Level 1 Full Supervision. |
Bitsch, Friedemann; Filax, Marco; Gonschorek, Tim; Ortmeier, Frank; Schumacher, Rolf Effiziente Sicherheitsnachweisführung mithilfe modellbasierter Systemanalyse Artikel Signal + Draht, 2017. @article{Bitsch2017, title = {Effiziente Sicherheitsnachweisf\"{u}hrung mithilfe modellbasierter Systemanalyse}, author = {Friedemann Bitsch and Marco Filax and Tim Gonschorek and Frank Ortmeier and Rolf Schumacher}, editor = {DVV Media Group}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/2017_BitschEtAl_EffizienteSicherheitsnachweisf\"{u}hrung.pdf}, year = {2017}, date = {2017-06-01}, journal = {Signal + Draht}, abstract = {This paper introduces a model-based computer-aided methodology for safety analyses in development and as- sessment processes for signalling and train control systems. The objective is to realise the application of model-based for- mal methods and simultaneously to reduce the outlay for us- ing them to a degree acceptable in industrial practice. Instead of performing safety analyses in parallel with the develop- ment process, existing system analyses and design models are used for deriving the necessary safety analyses models as au- tomatically as possible. Therefore, statements on safety and correctness can already be calculated in early development phases with precise results. Those early statements are deci- sive, because they make it possible to adapt and correct the system design at an early stage and to do it cost-efficiently.}, keywords = {}, pubstate = {published}, tppubtype = {article} } This paper introduces a model-based computer-aided methodology for safety analyses in development and as- sessment processes for signalling and train control systems. The objective is to realise the application of model-based for- mal methods and simultaneously to reduce the outlay for us- ing them to a degree acceptable in industrial practice. Instead of performing safety analyses in parallel with the develop- ment process, existing system analyses and design models are used for deriving the necessary safety analyses models as au- tomatically as possible. Therefore, statements on safety and correctness can already be calculated in early development phases with precise results. Those early statements are deci- sive, because they make it possible to adapt and correct the system design at an early stage and to do it cost-efficiently. |
Filax, Marco; Gonschorek, Tim; Ortmeier, Frank QuadSIFT: Unwrapping Planar Quadrilaterals to Enhance Feature Matching Inproceedings Proceedings of the 25rd International Conference in Central Europe on Computer Graphics, Visualization and Computer Vision, WSCG 2017 - Short Papers Proceedings, 2017. @inproceedings{filax17-wscg, title = {QuadSIFT: Unwrapping Planar Quadrilaterals to Enhance Feature Matching}, author = {Marco Filax and Tim Gonschorek and Frank Ortmeier}, url = {http://wscg.zcu.cz/wscg2017/short/I07-full.PDF https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/wscg2017_FilaxEtAl_QuadSIFT.pdf}, year = {2017}, date = {2017-01-01}, booktitle = {Proceedings of the 25rd International Conference in Central Europe on Computer Graphics, Visualization and Computer Vision, WSCG 2017 - Short Papers Proceedings}, volume = {25}, abstract = {Feature matching is one of the fundamental issues in computer vision. The established methods, however, do not provide reliable results, especially for extreme viewpoint changes. Different approaches have been proposed to lower this hurdle, e. g., by randomly sampling different viewpoints to obtain better results. However, these methods are computationally intensive. In this paper, we propose an algorithm to enhance image matching under the assumption that an image, taken in man-made environments, typically contains planar, rectangular objects. We use line segments to identify image patches and compute a homography which unwraps the perspective distortion for each patch. The unwrapped image patches are used to detect, describe and match SIFT features. We evaluate our results on a series of slanted views of a magazine and augmented reality markers. Our results demonstrate, that the proposed algorithm performs well for strong perspective distortions.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Feature matching is one of the fundamental issues in computer vision. The established methods, however, do not provide reliable results, especially for extreme viewpoint changes. Different approaches have been proposed to lower this hurdle, e. g., by randomly sampling different viewpoints to obtain better results. However, these methods are computationally intensive. In this paper, we propose an algorithm to enhance image matching under the assumption that an image, taken in man-made environments, typically contains planar, rectangular objects. We use line segments to identify image patches and compute a homography which unwraps the perspective distortion for each patch. The unwrapped image patches are used to detect, describe and match SIFT features. We evaluate our results on a series of slanted views of a magazine and augmented reality markers. Our results demonstrate, that the proposed algorithm performs well for strong perspective distortions. |
2016 |
Filax, Marco; Gonschorek, Tim; Ortmeier, Frank Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models Inproceedings Publishing, Springer International (Hrsg.): Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, S. 106 - 122, 2016, ISBN: 978-3-319-33951-1. @inproceedings{MF16-RSSR, title = {Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models}, author = {Marco Filax and Tim Gonschorek and Frank Ortmeier }, editor = {Springer International Publishing }, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/RSSR_CorrectFormalizationOfRequirementSpecifications.pdf}, doi = {10.1007/978-3-319-33951-1_8}, isbn = {978-3-319-33951-1}, year = {2016}, date = {2016-06-15}, booktitle = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings}, pages = {106 - 122}, abstract = {In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model. This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered. The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model. This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered. The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain. |
Filax, Marco; Gonschorek, Tim; Hebecker, Tanja; Lipaczewski, Michael; Madalinski, Agnes; Ortmeier, Frank; Fietze, Mario; Schumacher, Rolf Der Eisenbahn Ingenieur, S. 24 -27, 2016. @article{ei2016, title = {Bringing formal methods “on the rail” - Modellbasierte Systemanalyse in der Sicherheitsnachweisf\"{u}hrung}, author = {Marco Filax and Tim Gonschorek and Tanja Hebecker and Michael Lipaczewski and Agnes Madalinski and Frank Ortmeier and Mario Fietze and Rolf Schumacher}, editor = {Verband Deutscher Eisenbahn-Ingenieure E.V.}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/Ver\"{o}ffentlichung-Eisenbahningeneur.pdf}, year = {2016}, date = {2016-01-01}, journal = {Der Eisenbahn Ingenieur}, pages = {24 -27}, abstract = {Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gef\"{a}hrdungsraten in sogenannte Sicherheitsintegrit\"{a}tslevel (SIL 1-4) eingestuft. In der europ\"{a}ischen Norm EN50129 besteht, f\"{u}r die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universit\"{a}t Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterst\"{u}tzender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktf\"{o}rmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge erm\"{o}glichen die Portierung einer nat\"{u}rlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollst\"{a}ndigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal \"{u}berpr\"{u}ft werden k\"{o}nnen. Bereits in fr\"{u}hen Entwicklungsphasen k\"{o}nnen automatisiert qualitative und quantitative Absch\"{a}tzungen \"{u}ber die Sicherheit und Zuverl\"{a}ssigkeit mit pr\"{a}zisen und aussagekr\"{a}ftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endg\"{u}ltigen, sicherheitstechnischen Bewertung durch vollst\"{a}ndige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gefährdungsraten in sogenannte Sicherheitsintegritätslevel (SIL 1-4) eingestuft. In der europäischen Norm EN50129 besteht, für die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universität Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterstützender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktförmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge ermöglichen die Portierung einer natürlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollständigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal überprüft werden können. Bereits in frühen Entwicklungsphasen können automatisiert qualitative und quantitative Abschätzungen über die Sicherheit und Zuverlässigkeit mit präzisen und aussagekräftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endgültigen, sicherheitstechnischen Bewertung durch vollständige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert. |
2014 |
Gonschorek, Tim; Filax, Marco; Lipaczewski, Michael; Ortmeier, Frank VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification Buchkapitel IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 63-64, 2014. @inbook{FODB:80901373, title = {VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification}, author = { Tim Gonschorek and Marco Filax and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/gonshorek_VECS_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.}, pages = {63-64}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } |
Filax, Marco; Gonschorek, Tim; Lipaczewski, Michael; Ortmeier, Frank On Traceability of Informal Specifications for Model-Based Verification Inproceedings IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment., S. 11-18, Magdeburg : Univ., 2014. @inproceedings{FODB:80901202, title = {On Traceability of Informal Specifications for Model-Based Verification}, author = { Marco Filax and Tim Gonschorek and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/filax_IMBSA_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment.}, pages = {11-18}, publisher = {Magdeburg : Univ.}, abstract = {Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization. |
Lipaczewski, Michael; Filax, Marco; Ortmeier, Frank Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis Inproceedings European Conference on Software Engineering Education. - Herzogenrath : Shaker, S. 217-228, 2014. @inproceedings{FODB:80901605, title = {Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis}, author = { Michael Lipaczewski and Marco Filax and Frank Ortmeier}, year = {2014}, date = {2014-01-01}, booktitle = {European Conference on Software Engineering Education. - Herzogenrath : Shaker}, pages = {217-228}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |