mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Filipovikj, Predrag
Publications (10 of 11) Show all publications
Filipovikj, P. (2019). Automated Approaches for Formal Verification of Embedded Systems Artifacts. (Doctoral dissertation). Västerås: Mälardalen University
Open this publication in new window or tab >>Automated Approaches for Formal Verification of Embedded Systems Artifacts
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
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.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2019
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 292
Keywords
embedded systems, Simulink, systems specifications, model-checking, formal verification
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-43408 (URN)978-91-7485-429-9 (ISBN)
Public defence
2019-06-17, Gamma, Mälardalens högskola, Västerås, 13:30 (English)
Opponent
Supervisors
Projects
VeriSpec
Available from: 2019-05-09 Created: 2019-05-09 Last updated: 2019-05-15Bibliographically approved
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
Open this publication in new window or tab >>Bounded Invariance Checking of Simulink Models
2019 (English)In: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, p. 2168-2177Conference paper, Published paper (Refereed)
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. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42803 (URN)10.1145/3297280.3297493 (DOI)2-s2.0-85065663281 (Scopus ID)
Conference
SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019
Available from: 2019-02-27 Created: 2019-02-27 Last updated: 2019-05-24Bibliographically approved
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).
Open this publication in new window or tab >>Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
2019 (English)In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, p. 92-103Conference paper, Published paper (Refereed)
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. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-42802 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Conference
ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019
Available from: 2019-02-27 Created: 2019-02-27 Last updated: 2019-06-27Bibliographically approved
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 Engineering: . Paper presented at 14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019 (pp. 92-103). SciTePress
Open this publication in new window or tab >>Specifying industrial system requirements using specification patterns: A case study of evaluation with practitioners
2019 (English)In: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering, SciTePress , 2019, p. 92-103Conference paper, Published paper (Refereed)
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 the 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, called PROPAS, and propose a small-size evaluation of the approach with practitioners, on a case study conducted in cooperation with Scania, Sweden, 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 to be practically usefull for the non-experts in formal methods.

Place, publisher, year, edition, pages
SciTePress, 2019
Keywords
Industrial Case Study, Pattern-Based Requirements Specification, Specification Patterns, Automobile manufacture, Computer aided analysis, Computer software selection and evaluation, Formal verification, Computer aided verifications, Heavy-load vehicles, Industrial development, Industrial software, Requirements specifications, System specification, Formal specification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-44881 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Conference
14th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2019, 4 May 2019 through 5 May 2019
Available from: 2019-07-11 Created: 2019-07-11 Last updated: 2019-07-11Bibliographically approved
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
Open this publication in new window or tab >>Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience
2018 (English)In: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 75, p. 1-20Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
Germany: , 2018
Keywords
SMT-based consistency analysis, model-checking-based consistency analysis
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41726 (URN)10.14279/tuj.eceasst.75 (DOI)ISSN 1863-2122 (ISBN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2018-12-20 Created: 2018-12-20 Last updated: 2018-12-20Bibliographically approved
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
Open this publication in new window or tab >>An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Show others...
2017 (English)In: 29th Nordic Workshop on Programming Theory NWPT'17, Turku, Finland , Finland: TUCS Lecture Notes , 2017, p. 40-43Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
Turku, Finland , Finland: TUCS Lecture Notes, 2017
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-37338 (URN)978-952-12-3608-2 (ISBN)
Conference
29th Nordic Workshop on Programming Theory NWPT'17, 01 Nov 2017, Turku, Finland , Finland
Projects
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)
Available from: 2017-11-28 Created: 2017-11-28 Last updated: 2018-10-31Bibliographically approved
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
Open this publication in new window or tab >>Analyzing Industrial Simulink Models by Statistical Model Checking
Show others...
2017 (English)Report (Other academic)
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.

Place, publisher, year, edition, pages
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University, 2017
Series
MRTC Reports, ISSN 1404-3041
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-35069 (URN)MDH-MRTC-316/2017-1-SE (ISRN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2017-03-27 Created: 2017-03-27 Last updated: 2019-05-08Bibliographically approved
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
Open this publication in new window or tab >>Automated SMT-based Consistency Checking of Industrial Critical Requirements
2017 (English)In: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, no 4, p. 15-28Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
United States: ACM, 2017
Keywords
Requirements Consistency Analysis, Formal Methods, SMT, Z3
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-38940 (URN)000424075800002 ()
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2018-05-15 Created: 2018-05-15 Last updated: 2019-05-09Bibliographically approved
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.
Open this publication in new window or tab >>Increasing Embedded Systems´ Quality through Automated Specification and Analysis of Requirements and Behavioral Models
2017 (English)In: 43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017, 2017Conference paper, Published paper (Refereed)
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-38645 (URN)
Conference
43rd International Conference on Current Trends in Theory and Practice of Computer Science SOFSEM 2017, 16 Jan 2017, Limerick, Ireland
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2018-03-02 Created: 2018-03-02 Last updated: 2018-03-02Bibliographically approved
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
Open this publication in new window or tab >>SMT-based Consistency Analysis of Industrial Systems Requirements
2017 (English)In: 32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 2017, Vol. F128005, p. 1272-1279Conference paper, Published paper (Refereed)
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. 

Keywords
Con-sistency analysis, SMT, Specification patterns, System requirements, TCTL, Z3
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-34092 (URN)2-s2.0-85020883869 (Scopus ID)
Conference
32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 03 Apr 2017, Marrakesh, Morocco
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2016-12-14 Created: 2016-12-13 Last updated: 2019-06-19Bibliographically approved
Organisations

Search in DiVA

Show all publications