mdh.sePublikasjoner
Endre søk
Link to record
Permanent link

Direct link
BETA
Filipovikj, Predrag
Publikasjoner (10 av 10) Visa alla publikasjoner
Filipovikj, P. (2019). Automated Approaches for Formal Verification of Embedded Systems Artifacts. (Doctoral dissertation). Västerås: Mälardalen University
Åpne denne publikasjonen i ny fane eller vindu >>Automated Approaches for Formal Verification of Embedded Systems Artifacts
2019 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
Abstract [en]

Modern embedded software is so large and complex that creating the necessary artifacts, including system requirements specifications and design-time models, as well as assuring their correctness have become difficult to manage. One challenge stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints, which make them hard to analyze. Another challenge is the quality assurance of various design-time models developed using Simulink as the de facto standard model-based development tool in the automotive domain, avionics domain, etc. Currently, the industrial state-of-practice resorts to simulation of Simulink models, which gives insight in the system’s behavior yet does not provide a high degree of assurance that the model behaves correctly. A potential way to address the aforementioned challenges is to apply computer-aided, mathematically-rigorous methods for specification, analysis and verification already at the requirements specification stage, but also at later development stages.

In this thesis, we propose a set of approaches for the formal specification, analysis and verification of system requirement specifications and design-time Simulink models, with particular focus on the automotive industry. Our contributions are as follows: first, we assess the expressiveness of an existing patternbased technique for the formal requirements specification on an operational system. Based on the positive findings, we deem the technique expressive enough to capture systems requirements in controlled natural language, from which formal counterparts can be automatically generated. To bring the approach closer to the practitioners we propose a tool, called PROPAS. Next, we propose an automated consistency analysis approach based on Satisfiability Modulo Theories for the system requirements specifications formally encoded as temporal logic formulas. The approach is implemented in our PROPAS tool and is suitable to analyze the lack of logical contradictions within the system specification, at early system development phases. Our next contribution addresses the formal analysis and verification of large Simulink models. First, we propose a pattern-based and execution-order-preserving approach for transforming Simulink models into networks of stochastic timed automata, which can be analyzed using the UPPAAL SMC tool that returns the probability that a property is satisfied by the model. For the automated generation of the analysis model, we propose the SIMPPAAL tool. Our second approach is based on bounded model checking and is suitable for checking invariance properties of Simulink models. Compared to the statistical model checking approach, the invariance checking is reduced to a satisfiability problem. In case of property violation, the procedure generates a counter-example execution trace, which can be used for refining the model. In the same work we show that there exist commonly-used design patterns in Simulink models, for which the verification result is complete. The approach is supported by our SYMC tool.

For validation of the specification patterns, and the PROPAS tool we perform a case-study evaluation with practitioners, in collaboration with our industrial partner Scania. The results show that the pattern-based approach and the PROPAS tool can be practically useful in industrial settings. We apply the statistical model-checking approach and the SIMPPAAL tool on two industrial use cases, namely Brake-by-Wire and Adjustable Speed Limiter from Volvo Group Trucks Technology, which yields encouraging results. Finally, we validate the bounded invariance-checking approach and the SYMC tool on the Brake-by-Wire system, where we demonstrate both complete and incomplete verification of invariance properties.

sted, utgiver, år, opplag, sider
Västerås: Mälardalen University, 2019
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 292
Emneord
embedded systems, Simulink, systems specifications, model-checking, formal verification
HSV kategori
Forskningsprogram
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-43408 (URN)978-91-7485-429-9 (ISBN)
Disputas
2019-06-17, Gamma, Mälardalens högskola, Västerås, 13:30 (engelsk)
Opponent
Veileder
Prosjekter
VeriSpec
Tilgjengelig fra: 2019-05-09 Laget: 2019-05-09 Sist oppdatert: 2019-05-15bibliografisk kontrollert
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2019). Bounded Invariance Checking of Simulink Models. In: Proceedings of the ACM Symposium on Applied Computing: . Paper presented at SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019 (pp. 2168-2177). , Part F147772
Åpne denne publikasjonen i ny fane eller vindu >>Bounded Invariance Checking of Simulink Models
2019 (engelsk)Inngår i: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, s. 2168-2177Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Currently, Simulink models can be verified rigorously against design errors or statistical properties. In this paper, we show how Simulink models can be formally analyzed against invariance properties using bounded model checking reduced to satisfiability modulo theories solving. In its basic form, the technique provides means for verification of an underlying model over bounded traces rigorously, however, in general the procedure is incomplete. We identify common Simulink block types and compositions by analyzing selected industrial models, and we show that for some of them the set of non-repeating states (reachability diameter) can be visited with a finite set of paths of finite length, yielding the verification complete. We complement our approach with a tool, called SyMC that automates the following: i) calculation of the reachability diameter size for some of the designs, ii) generation of finite (bounded) paths of the underlying Simulink model and their encoding into SMT-LIB format and iii) checking invariance properties using the Z3 SMT solver. To show the applicability of our approach, we apply it on a prototype implementation of an industrial Simulink model, namely Brake by Wire from Volvo Group Trucks Technology, Sweden. 

HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-42803 (URN)10.1145/3297280.3297493 (DOI)000474685800302 ()2-s2.0-85065663281 (Scopus ID)
Konferanse
SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019
Tilgjengelig fra: 2019-02-27 Laget: 2019-02-27 Sist oppdatert: 2019-10-11bibliografisk kontrollert
Filipovikj, P. & Seceleanu, C. (2019). Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners. In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019: . Paper presented at ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019 (pp. 92-103).
Åpne denne publikasjonen i ny fane eller vindu >>Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
2019 (engelsk)Inngår i: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, s. 92-103Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

With the ever-increasing size and complexity of the industrial software systems there is an imperative need for an automated, systematic and exhaustive verification of various software artifacts, such as system specifications, models, code, etc. A potential remedy for this need might lie in a pool of techniques for computer-aided verification of software related artifacts, including system specifications. The Achilles' heel of these techniques, and the main hinder for their wider adoption in industrial development process are the complexity and the specialized skill-set required for the formal encoding of specifications. To alleviate this problem, Specification Patterns that are based on the observation that the system specifications are framed within reoccurring solutions have been proposed. The approach has been shown to be expressive enough for capturing requirements in the automotive domain, however, there is a lack of empirical data that can be used to judge its practical usefulness. In this paper, we involve an existing specification-patterns-based tool, and propose a small-size evaluation of the approach with practitioners, on a case study conducted in cooperation with Scania, one of the world's leading manufacturers of heavy-load vehicles. Our results show that the specification patterns that are supported by an adequate tooling have the potential for adoption in industrial practice. 

HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-42802 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Konferanse
ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019
Tilgjengelig fra: 2019-02-27 Laget: 2019-02-27 Sist oppdatert: 2019-06-27bibliografisk kontrollert
Filipovikj, P., Rodriguez-Navas, G. & Seceleanu, C. (2018). Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience. Electronic Communications of the EASST, 75, 1-20
Åpne denne publikasjonen i ny fane eller vindu >>Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience
2018 (engelsk)Inngår i: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 75, s. 1-20Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

Industry relies predominantly on manual peer-review techniques for assessing the correctness of system specifications. However, with the ever-increasing size, complexity and intricacy of specifications, it becomes difficult to assure their correctness with respect to certain criteria such as consistency. To address this challenge, a technique called sanity checking has been proposed. The goal of the technique is to assess the quality of the system specification in a systematic and rigorous manner with respect to a formally-defined criterion. Predominantly, the sanity checking criteria, such as for instance consistency, are encoded as reachability or liveness properties which can then be verified via model checking. Recently, a complementary approach for checking the consistency of a system's specification by reducing it to a satisfiability problem that can be analyzed using Satisfiability Modulo Theories has been proposed. In this paper, we compare the two approaches for consistency analysis, by applying them on a relevant industrial use case, using the same definition for consistency and the same set of requirements. Since the bottlenecks of analyzing large systems formally are most often the construction of the model and the time needed to return a verdict, we carry out the comparison with respect to the: i) required effort for generating the analysis model and the latter's complexity, and ii) consistency analysis time. Assuming checking only invariance properties, our results show no significant difference in analysis time between the two approaches when applied on the same system specification under the same definition of consistency. As expected, the main difference between the two comes from the required time and effort of creating the analysis models.

sted, utgiver, år, opplag, sider
Germany: , 2018
Emneord
SMT-based consistency analysis, model-checking-based consistency analysis
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-41726 (URN)10.14279/tuj.eceasst.75 (DOI)ISSN 1863-2122 (ISBN)
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tilgjengelig fra: 2018-12-20 Laget: 2018-12-20 Sist oppdatert: 2018-12-20bibliografisk kontrollert
Marinescu, R., Filipovikj, P., Enoiu, E. P., Larsson, J. & Seceleanu, C. (2017). An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models. In: 29th Nordic Workshop on Programming Theory NWPT'17: . Paper presented at 29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland (pp. 40-43). Turku, Finland , Finland: TUCS Lecture Notes
Åpne denne publikasjonen i ny fane eller vindu >>An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Vise andre…
2017 (engelsk)Inngår i: 29th Nordic Workshop on Programming Theory NWPT'17, Turku, Finland , Finland: TUCS Lecture Notes , 2017, s. 40-43Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system’s structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. Modern embedded systems, such as autonomous vehicles and robots, have low-energy computing demands, making testing for energy usage increasingly important. Nevertheless, testing resource-aware properties of architectural models has received less attention than the functional testing of such models. In our previous work, we have outlined a method for testing energy consumption in embedded systems using manually created faults based on statistical model checking of a priced formal system model. In this paper, we extend our previous work by showing how mutation testing] can be used to generate and select test cases based on the concept of energy-aware mutants– small syntactic modifications in the architectural model, intended to mimic real energy faults. Test cases that can distinguish a certain behavior from its mutations are sensitive to changes in the model, and hence considered to be good at detecting faults. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.

sted, utgiver, år, opplag, sider
Turku, Finland , Finland: TUCS Lecture Notes, 2017
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-37338 (URN)978-952-12-3608-2 (ISBN)
Konferanse
29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyCAMI - Artificially intelligent ecosystem for self-management and sustainable quality of life in AAL (Ambient Assisted Living)DPAC - Dependable Platforms for Autonomous systems and ControlMegaMaRt2 - Megamodelling at Runtime (ECSEL/Vinnova)
Tilgjengelig fra: 2017-11-28 Laget: 2017-11-28 Sist oppdatert: 2018-10-31bibliografisk kontrollert
Filipovikj, P., Mahmud, N., Marinescu, R., Rodriguez-Navas, G., Seceleanu, C., Ljungkrantz, O. & Lönn, H. (2017). Analyzing Industrial Simulink Models by Statistical Model Checking. Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University
Åpne denne publikasjonen i ny fane eller vindu >>Analyzing Industrial Simulink Models by Statistical Model Checking
Vise andre…
2017 (engelsk)Rapport (Annet vitenskapelig)
Abstract [en]

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose a pattern-based, execution-order preserving automatic transformation of Simulink atomic and composite blocks into stochastic timed automata that can then be analyzed formally with UPPAAL Statistical Model Checker (UPPPAAL SMC). Our method is supported by the tool SIMPPAAL, which we also introduce and apply on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

sted, utgiver, år, opplag, sider
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University, 2017
Serie
MRTC Reports, ISSN 1404-3041
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-35069 (URN)MDH-MRTC-316/2017-1-SE (ISRN)
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tilgjengelig fra: 2017-03-27 Laget: 2017-03-27 Sist oppdatert: 2019-05-08bibliografisk kontrollert
Filipovikj, P., Rodriguez-Navas, G., Nyberg, M. & Seceleanu, C. (2017). Automated SMT-based Consistency Checking of Industrial Critical Requirements. ACM SIGAPP Applied Computing Review, 17(4), 15-28
Åpne denne publikasjonen i ny fane eller vindu >>Automated SMT-based Consistency Checking of Industrial Critical Requirements
2017 (engelsk)Inngår i: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, nr 4, s. 15-28Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

With the ever-increasing size, complexity and intricacy of system requirements specifications, it becomes difficult to ensure their correctness with respect to certain criteria such as consistency. Automated formal techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. Sometimes such techniques incur a high modeling cost or analysis time, or are not applicable. To address such problems, in this paper we propose an automated consistency analysis technique of requirements that are formalized based on patterns, and checked using state-of-the-art Satisfiability Modulo Theories solvers. Our method assumes several transformation steps, from textual requirements to formal logic, and next into the format suited for the SMT tool. To automate such steps, we propose a tool, called PROPAS, that does not require any user intervention during the transformation and analysis phases, thus making the consistency analysis usable by non-expert practitioners. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive system called the Fuel Level Display.

sted, utgiver, år, opplag, sider
United States: ACM, 2017
Emneord
Requirements Consistency Analysis, Formal Methods, SMT, Z3
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-38940 (URN)000424075800002 ()
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tilgjengelig fra: 2018-05-15 Laget: 2018-05-15 Sist oppdatert: 2019-05-09bibliografisk kontrollert
Filipovikj, P. (2017). Increasing Embedded Systems´ Quality through Automated Specification and Analysis of Requirements and Behavioral Models. In: 43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017: . Paper presented at 43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017, 16 Jan 2017, Limerick, Ireland.
Åpne denne publikasjonen i ny fane eller vindu >>Increasing Embedded Systems´ Quality through Automated Specification and Analysis of Requirements and Behavioral Models
2017 (engelsk)Inngår i: 43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017, 2017Konferansepaper, Publicerat paper (Fagfellevurdert)
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-38645 (URN)
Konferanse
43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017, 16 Jan 2017, Limerick, Ireland
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tilgjengelig fra: 2018-03-02 Laget: 2018-03-02 Sist oppdatert: 2018-03-02bibliografisk kontrollert
Filipovikj, P., Rodriguez-Navas, G., Nyberg, M. & Seceleanu, C. (2017). SMT-based Consistency Analysis of Industrial Systems Requirements. In: 32nd ACM SIGAPP Symposium On Applied Computing SAC2017: . Paper presented at 32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 03 Apr 2017, Marrakesh, Morocco (pp. 1272-1279). , F128005
Åpne denne publikasjonen i ny fane eller vindu >>SMT-based Consistency Analysis of Industrial Systems Requirements
2017 (engelsk)Inngår i: 32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 2017, Vol. F128005, s. 1272-1279Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

As the complexity of industrial systems increases, it becomes dificult to ensure the correctness of system requirements specifications with respect to certain criteria such as consistency. Automated techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. However, such approaches can some-times be costly in terms of modeling and analysis time or not applicable for certain types of properties. In this paper, we present a complementary method that relies on pattern-based formalization of requirements and automated consistency checking using the state-of-the-art SMT tool Z3. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive subsystem called the Fuel Level Display. 

Emneord
Con-sistency analysis, SMT, Specification patterns, System requirements, TCTL, Z3
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-34092 (URN)2-s2.0-85020883869 (Scopus ID)
Konferanse
32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 03 Apr 2017, Marrakesh, Morocco
Prosjekter
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tilgjengelig fra: 2016-12-14 Laget: 2016-12-13 Sist oppdatert: 2019-06-19bibliografisk kontrollert
Filipovikj, P., Nyberg, M. & Rodriguez-Navas, G. (2014). Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain. In: 2014 IEEE 22ND INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE): . Paper presented at IEEE 22nd International Requirements Engineering Conference (RE), AUG 25-29, 2014, Blekinge Inst Technol, Karlskrona, SWEDEN (pp. 444-450). IEEE
Åpne denne publikasjonen i ny fane eller vindu >>Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain
2014 (engelsk)Inngår i: 2014 IEEE 22ND INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE), IEEE , 2014, s. 444-450Konferansepaper (Fagfellevurdert)
Abstract [en]

The importance of using formal methods and techniques for verification of requirements in the automotive industry has been greatly emphasized with the introduction of the new ISO26262 standard for road vehicles functional safety. The lack of support for formal modeling of requirements still represents an obstacle for the adoption of the formal methods in industry. This paper presents a case study that has been conducted in order to evaluate the difficulties inherent to the process of transforming the system requirements from their traditional written form into semi-formal notation. The case study focuses on a set of non-structured functional requirements for the Electrical and Electronic (E/E) systems inside heavy road vehicles, written in natural language, and reassesses the applicability of the extended Specification Pattern System (SPS) represented in a restricted English grammar. Correlating this experience with former studies, we observe that, as previously claimed, the concept of patterns is likely to be generally applicable for the automotive domain. Additionally, we have identified some potential difficulties in the transformation process, which were not reported by the previous studies and will be used as a basis for further research.

sted, utgiver, år, opplag, sider
IEEE, 2014
Serie
Proceedings of International Requirements Engineering, ISSN 1097-0592
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-38376 (URN)000363280400055 ()978-1-4799-3033-3 (ISBN)
Konferanse
IEEE 22nd International Requirements Engineering Conference (RE), AUG 25-29, 2014, Blekinge Inst Technol, Karlskrona, SWEDEN
Tilgjengelig fra: 2018-02-12 Laget: 2018-02-12 Sist oppdatert: 2019-05-09bibliografisk kontrollert
Organisasjoner