| 1. |
- Claessen, Koen, 1975, et al.
(författare)
-
Applying valued booleans in testing of cyber-physical systems
- 2018
-
Ingår i: Proceedings - 2018 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT-CPS 2018. ; , s. 8-9
-
Konferensbidrag (refereegranskat)abstract
- In software testing, as in cyber-physical systems testing, test suites are traditionally developed by hand. In this work we consider one framework for putting the computer in charge of the testing instead: constrained random test case generation as supported by the tool QuickCheck. This is implemented by the use of Valued Booleans (VBools). VBools naturally allow for an extension of QuickCheck into cyber-physical systems, which is useful particularly since QuickCheck can perform shrinking of test cases. Shrinking is a technique to make test cases simpler while preserving failure.
|
|
| 2. |
- Ebrahimi, Amir Hossein, 1976, et al.
(författare)
-
Automated analysis of interdependencies between product platforms and assembly operations
- 2016
-
Ingår i: Procedia CIRP. - : Elsevier BV. - 2212-8271. ; 44, s. 67-72
-
Konferensbidrag (refereegranskat)abstract
- Configurable products, like vehicles, face the challenge of handling all possible variants which are needed to answer the various customer needs. For these configurable products the support of all variants need to be addressed both by the design phase and the production phase. The product design phase and the production phase are linked together via operations. These operations model how each part of the bill-of-material is assembled to the final product. Operations also have inner relations among themselves, namely the precedence constraints, stating the order in which different parts can be assembled. Considering only the precedence constraints a product can generally be assembled in various different ways. It is through line balancing that the operations are assigned to different stations and/or assembly workers. The bill-of-material for each configurable product might be different with each variant, which will result in different set of operations. However, due to the precedence rules among the operations not all sets of operations might be possible to complete. The contribution in this paper is a automated method that can determine if all possible product variants can be successfully assembled while still satisfying precedence constraints between operations. The paper also includes an industrial example which further exemplifies the needed input for the method and the possible method outputs as a result of introducing a new variant to the product platform.
|
|
| 3. |
- Ebrahimi, Amir Hossein, 1976, et al.
(författare)
-
Formal analysis of product variability and the effects on assembly operations
- 2015
-
Ingår i: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. - 1946-0759 .- 1946-0740. - 9781467379298 ; 2015-October
-
Konferensbidrag (refereegranskat)abstract
- A challenge for highly configurable products, like vehicles, is that the product system has to support all possible variants that can be configured by a customer. The production system is often highly automated with software in robots, machines and programmable logic controllers that need to be prepared to handle all possible variants. The link between the product and the assembly system can be expressed through operations where each operation models how a part in the bill-of-material is assembled to the product to be built. Typically the operations have precedence constraints that express that certain parts have to be assembled before other parts might be assembled. Given only the precedence constraints a product can generally be assembled in many different ways and through line balancing the operations are assigned to different stations, machines, and/or assembly workers. For configurable products the bill-of-material might be different for each variant, consequently the necessary operations will be different. However, since the operations have precedence constraints we have to make sure that all possible variants can be successfully assembled while still satisfying all precedence constraints. The contribution in this paper is a fully automated novel method that can determine if all possible product variants can be successfully assembled while still satisfying precedence constraints between operations.
|
|
| 4. |
- Eddeland, Johan, 1991, et al.
(författare)
-
Automated Mode Coverage Analysis for Cyber-Physical Systems using Hybrid Automata
- 2017
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 50:1, s. 9260-9265
-
Konferensbidrag (refereegranskat)abstract
- Testing of cyber-physical systems (CPSs) is a complex task, mainly due to the presence of continuous dynamics. In industry, CPSs are typically safety-critical and their complexity is rapidly increasing. Thus, it is important to know how well the tests perform. One common approach to ensuring test quality is to use coverage criteria, for example the well-known MC/DC. However, most of the used coverage criteria in industry depend on code structure to find errors in the system and may fail to capture the complete dynamical behaviour. Two coverage definitions are presented that can be used to ensure that all the continuous dynamics in the system have been explored. It is shown that the MC/DC criterion is not always rigorous enough to test all the system behaviour. Finally, the proposed coverage criteria are applied to automatically assess the test quality for a plant model used at Volvo Car Corporation.
|
|
| 5. |
- Eddeland, Johan, 1991, et al.
(författare)
-
Objective functions for falsification of signal temporal logic properties in cyber-physical systems
- 2017
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. - 9781509067817 ; 2017-August, s. 1326-1331
-
Konferensbidrag (refereegranskat)abstract
- Cyber-physical systems, such as automation and automotive systems, are highly complex systems that are frequently also safety-critical. Thus, it is important that these systems behave as intended, as incorrectness can have serious consequences. Due to continuous dynamics that yield infinite state spaces, the systems cannot be exhaustively tested to guarantee correct behavior, but systematic testing can be used to systematically search for behavior that is inconsistent with the requirements. However, manual testing is a tedious and error-prone task, and thus it is desirable to automate as much of the testing process as possible to increase efficiency and eliminate manual errors. This paper considers falsification of requirements expressed as temporal logic formulae to find errors in the Model-in-the-Loop stage of model-based development. The falsification is an optimization procedure where the objective function is determined by the definition of a quantitative semantics for the temporal logic formalism, and the optimization is performed over an input parametrization. It is shown that in certain cases where the discreteness of the system under test manifests itself in the objective function, the robustness values for the temporal logic specifications need to be modified. This paper presents two alternative objective functions suitable for these cases, and illustrates their use with both a small example and a use case from Volvo Car Corporation.
|
|
| 6. |
|
|
| 7. |
- Fei, Zhennan, 1984, et al.
(författare)
-
A BDD-Based Approach for Designing Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems
- 2015
-
Ingår i: IEEE Transactions on Automation Science and Engineering. - 1558-3783 .- 1545-5955. ; 12:3, s. 990-1006
-
Tidskriftsartikel (refereegranskat)abstract
- In order to develop a computationally efficient implementation of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), a recent approach focuses on the identification of a set of critical states of the underlying RAS state-space, referred to as minimal boundary unsafe states. The availability of this information enables an expedient one-step-lookahead scheme that prevents the RAS from reaching outside its safe region. The work presented in this paper seeks to develop a symbolic approach, based on binary decision diagrams (BDDs), for efficiently retrieving the (minimal) boundary unsafe states from the underlying RAS state-space. The presented results clearly demonstrate that symbolic computation enables the deployment of the maximally permissive DAP for complex RAS with very large structure and state-spaces with limited time and memory requirements. Furthermore, the involved computational costs are substantially reduced through the pertinent exploitation of the special structure that exists in the considered problem.
|
|
| 8. |
- Fei, Zhennan, 1984, et al.
(författare)
-
Symbolic computation and representation of deadlock avoidance policies for complex resource allocation systems with application to multithreaded software
- 2015
-
Ingår i: Proceedings of the IEEE Conference on Decision and Control. - 0743-1546 .- 2576-2370. ; 2015-February, s. 5935-5942
-
Konferensbidrag (refereegranskat)abstract
- In our recent work, we proposed a series of binary decision diagram (BDD-) based approaches for developing the maximally permissive deadlock avoidance policy (DAP) for a class of complex resource allocation systems (RAS). In this paper, (i) we extend these approaches by introducing a procedure that generates a set of comprehensible 'guard' predicates to represent the resulting DAP, and (ii) we customize them to the problem of deadlock avoidance in shared-memory multithreaded software, that has been previously addressed by the Gadara project. In the context of this last application, the generated guards can be instrumented directly into the source code of the underlying software threads, providing, thus, a very efficient and natural representation of the target policy. At the same time, by integrating the representational and computational strengths of symbolic computation, the presented approach can support the computation of the maximally permissive DAP for RAS corresponding to problem instances of even larger scale and complexity than those addressed in the current literature.
|
|
| 9. |
- Fei, Zhennan, 1984, et al.
(författare)
-
Symbolic computation of boundary unsafe states in complex resource allocation systems using partitioning techniques
- 2015
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. - 9781467381833 ; 2015-October, s. 799-806
-
Konferensbidrag (refereegranskat)abstract
- In some recent work, we proposed a binary decision diagram (BDD-) based approach for the development of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), that is based on the identification and the explicit storage of a set of critical states in the underlying RAS state-space. The work presented in this paper seeks to extend the applicability of the aforementioned results by coupling them with a partitioning technique for the more efficient storage and processing of the BDD that encodes the underlying state space. The reported numerical experimentation demonstrates the increased efficiency of the new algorithm w.r.t. its space and time complexity, compared to the previous method that uses a more monolithic representation of the RAS state-space. The last part of the paper also discusses some further potential advantages of the presented method, including its amenability to a parallelized implementation and its ability to cope effectively and efficiently with uncontrollable behavior.
|
|
| 10. |
- Li, Jason, 1993, et al.
(författare)
-
Evaluation of Photogrammetry for Use in Industrial Production Systems
- 2018
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. ; 2018-August, s. 414-420
-
Konferensbidrag (refereegranskat)abstract
- A digital twin of a production system consists of geometric, kinematic and logical models of the physical system. One of the key challenges is to keep the digital twin up-to-date with changes of the real one. Today, laser scanning is the de-facto standard used to keep the geometry of the digital model synchronized. In recent years, advancements in the performance of Graphic Processing Units (GPUs) and the availability of cheap high-resolution digital cameras have made photogrammetry a viable alternative to laser scanning for building digital 3D-models. In this study, we investigate how photogrammetry competes against laser-scanning by comparing their results in form of point-clouds.
|
|
