A methodology for verifying SysML requirements using activity diagrams

Designing complex and critical systems needs a methodology to ensure the correctness of their specifications. Within an overall approach which considers the validation of SysML designs, this paper proposes a methodology for verifying SysML requirements on activity diagrams. The objective is to define a complete process to formalize and verify SysML functional requirements related to activity diagrams. Our contributions lie, first, in the definition of AcTRL (Activity Temporal Requirement Language), a new language for the formalization of functional requirements at SysML level. Second, in the proposed verification methodology which is guided by the Open image in new window verify Open image in new window relationships between SysML requirements and activity diagrams. The verification is enabled by formalizing SysML activities with hierarchical coloured Petri nets (HCPNs) and by automatically translating SysML requirements expressed on AcTRL into temporal logic. Our methodology takes into account the hierarchical structure of SysML activities and their relations with SysML requirements to provide a modular and incremental verification. A case study for a ticket vending machine is presented to illustrate the different steps and the benefits of the proposed methodology.     

A formal verification framework for SysML activity diagrams

SysML activity diagrams are OMG/INCOSE standard diagrams used for modeling and specifying probabilistic systems. They support systems composition by call behavior and send/receive artifacts. For verification, the existing approaches dedicated to these diagrams are limited to a restricted set of artifacts. In this paper, we propose a formal verification framework for these diagrams that supports the most important artifacts. It is based on mapping a composition of SysML activity diagrams to the input language of the probabilistic symbolic model checker called “PRISM”. To prove the soundness of our mapping approach, we capture the underlying semantics of both the SysML activity diagrams and their generated PRISM code. We found that the probabilistic equivalence relation between both semantics preserve the satisfaction of the system requirements. Finally, we demonstrate the effectiveness of our approach by presenting real case studies.     

Quantitative and qualitative analysis of SysML activity diagrams

Model-driven engineering refers to a range of approaches that uses models throughout systems and software development life cycle. Towards sustaining such a successful approach in practice, we present a model-based verification framework that supports the quantitative and qualitative analysis of SysML activity diagrams. To this end, we propose an algorithm that maps SysML activity diagrams into Markov decision processes expressed using the language of the probabilistic symbolic model checker PRISM. Furthermore, we elaborate on the correctness of our translation algorithm by proving its soundness with respect to a SysML activity diagrams operational semantics that we also present in this work. The generated models can be verified against a set of properties expressed in the probabilistic computation tree logic. To automate our approach, we developed a prototype tool that interfaces a modeling environment and the probabilistic model checker. We also show how to leverage adversary generation to provide the developer with a useful counterexample/witness as a feedback on the verified properties. Finally, the established theoretical foundations are complemented with an illustrative case study that demonstrates the usability and benefit of such a framework.     

Contract-based modeling and verification of timed safety requirements within SysML

In order to cope with the growing complexity of critical real-time embedded systems, systems engineering has adopted a component-based design technique driven by requirements. Yet, such an approach raises several issues since it does not explicitly prescribe how system requirements can be decomposed on components nor how components contribute to the satisfaction of requirements. The envisioned solution is to design, with respect to each requirement and for each involved component, an abstract specification, tractable at each design step, that models how the component is concerned by the satisfaction of the requirement and that can be further refined toward a correct implementation. In this paper, we consider such specifications in the form of contracts. A contract for a component consists in a pair (assumption, guarantee) where the assumption models an abstract behavior of the component’s environment and the guarantee models an abstract behavior of the component given that the environment behaves according to the assumption. Therefore, contracts are a valuable asset for the correct design of systems, but also for mapping and tracing requirements to components, for tracing the evolution of requirements during design and, most importantly, for compositional verification of requirements. The aim of this paper is to introduce contract-based reasoning for the design of critical real-time systems made of reactive components modeled with UML and/or SysML. We propose an extension of UML and SysML languages with a syntax and semantics for contracts and the refinement relations that they must satisfy. The semantics of components and contracts is formalized by a variant of timed input/output automata on top of which we build a formal contract-based theory. We prove that the contract-based theory is sound and can be applied for a relatively large class of SysML system models. Finally, we show on a case study extracted from the automated transfer vehicle (http://www.esa.int/ATV) that our contract-based theory allows to verify requirement satisfaction for previously intractable models.     

基于有色Petri网的SysML序列图的分析与验证

针对SysML序列图本身缺乏分析和验证手段的问题,提出了一种序列图到有色Petri网的转换方法:定义了将序列图的常用操作转换为等价有色Petri网的转换规则,重点是把序列图的常用结构如可选结构、条件结构、并行结构以及循环结构等映射为有色Petri网。这当中既包含结构元素,如库所、变迁、输入/输出弧,又包含逻辑元素,如全局声明中的颜色集和变量、颜色集与库所、弧表达式以及初始标志。应用这些规则可以将序列图转换为有色Petri网模型,进而对其进行仿真分析,并可通过有色Petri网工具验证模型的无死锁性、可达性、有界性和活性。最后通过数字证书更新的实例分析了映射前后两种模型的语义,验证了映射的正确性。     

A framework to specify system requirements using natural interpretation of UML/MARTE diagrams

Software and Systems Modeling - The ever-increasing design complexity of embedded systems is constantly pressing the demand for more abstract design levels and possible methods for automatic...     

A new approach to combine texture compression and filtering

Texture mapping has been widely used to improve the quality of 3D rendered images. To reduce the storage and bandwidth impact of texture mapping, compression systems are commonly used. To further increase the quality of the rendered images, texture filtering is also often adopted. These two techniques are generally considered to be independent. First, a decompression step is executed to gather texture samples, which is then followed by a separate filtering step. We have investigated a system based on linear transforms that merges both phases together. This allows more efficient decompression and filtering at higher compression ratios. This paper formally presents our approach for any linear transformation, how the commonly used discrete cosine transform can be adapted to this new approach, and how this method can be implemented in real time on current-generation graphics cards using shaders. Through reuse of the existing hardware filtering, fast magnification and minification filtering is achieved. Our implementation provides fully anisotropically filtered samples four to six times faster than an implementation using two separate phases for decompression and filtering. Additionally, our transform-based compression also provides increased and variable compression ratios over standard hardware compression systems at a comparable or better quality level.     

A rewriting approach to binary decision diagrams

Binary decision diagrams (BDDs) provide an established technique for propositional formula manipulation. In this paper, we present the basic BDD theory by means of standard rewriting techniques. Since a BDD is a DAG instead of a tree we need a notion of shared rewriting and develop appropriate theory. A rewriting system is presented by which canonical reduced ordered BDDs (ROBDDs) can be obtained and for which uniqueness of ROBDD representation is proved. Next, an alternative rewriting system is presented, suitable for actually computing ROBDDs from formulas. For this rewriting system a layerwise strategy is defined, and it is proved that when replacing the classical apply-algorithm by layerwise rewriting, roughly the same complexity bound is reached as in the classical algorithm. Moreover, a layerwise innermost strategy is defined and it is proved that the full classical algorithm for computing ROBDDs can be replaced by layerwise innermost rewriting without essentially affecting the complexity. Finally a lazy strategy is proposed sometimes performing much better than the traditional algorithm.     

A new DFM approach to combine machining and additive manufacturing

Design for manufacturing (DFM) approaches aim to integrate manufacturability aspects during the design stage. Most of DFM approaches usually consider only one manufacturing process, but product competitiveness may be improved by designing hybrid modular products, in which products are seen as 3-D puzzles with modules realized individually by the best manufacturing process and further gathered. A new DFM system is created in order to give quantitative information during the product design stage of which modules will benefit in being machined and which ones will advantageously be realized by an additive process (such as Selective Laser Sintering or laser deposition). A methodology for a manufacturability evaluation in case of a subtractive or an additive manufacturing process is developed and implemented in a CAD software. Tests are carried out on industrial products from automotive industry.     

A factorization approach to evaluating simultaneous influence diagrams

Evaluating an influence diagram (ID) is a challenging problem because its complexity increases exponentially in the number of decision nodes in the diagram. In this paper, we examine the problem for a special class of IDs where multiple decisions must be made simultaneously. We describe a brief theory that factorizes out the computations common to all policies in evaluating them. Our evaluation approach conducts these computations once and uses them across all policies. We identify the ID structures for which the approach can achieve savings. We show that the approach can be used to efficiently recompute the optimal policy of an ID when its structure or parameters change. Finally, we demonstrate the superior performance of the approach by simulation studies and a military planning example.     

A first attempt at assimilating microwave-derived SST to improve the predictive capability of a coupled,high-resolution Eta-POM forecasting system

This study implements the assimilation of sea surface temperature (SST) data acquired by passive microwave remote sensing to a high-resolution, primitive-equation ocean model. The aim was to improve a forecasting tool capable of predicting the surface ocean processes linked to the air–sea interactions at sub-mesoscale level using one-way coupled, atmosphere–ocean modelling. An assimilation scheme based on a Newtonian relaxation scheme was fine-tuned to improve the forecasting skill of the ocean model. The ocean model was driven by predicted, synchronous air–sea fluxes derived by an overlying atmosphere model, remotely sensed SST and lateral boundary conditions derived from its previous run. The estimation of the model forecasting error was based on statistical and spatial comparison with remotely sensed observations. The optimal nudging coefficient was found to be 5 × 10^?4 for 12 hours, giving a mean bias of ?0.07°C. Forecast validation was done against calibrated AVHRR scenes using a new approach to calibrate region-specific scenes based on the split-window technique. This work demonstrates the benefit of using passive microwave remote sensing to improve high-resolution ocean forecasting systems. It also shows the high complementarity of infrared and passive microwave satellite sensors to provide information on the surface thermodynamics of the Ionian Sea.     

A list-processing approach to compute Voronoi diagrams and theEuclidean distance transform

We propose an efficient Voronoi transform algorithm for constructing Voronoi diagrams using segment lists of rows. A significant feature of the algorithm is that it takes segments rather than pixels as the basic units to represent and propagate the nearest neighbor information. The segment lists are dynamically updated as they are scanned. A distance map can then be easily computed from the segment list representation of the Voronoi diagram. Experimental results have demonstrated its high efficiency. Extension of the algorithm to higher dimensions is also discussed     

A profile and tool for modelling safety information with design information in SysML

Communication both between development teams and between individual developers is a common source of safety-related faults in safety–critical system design. Communication between experts in different fields can be particularly challenging due to gaps in assumed knowledge, vocabulary and understanding. Faults caused by communication failures must be removed once found, which can be expensive if they are found late in the development process. Aiding communication earlier in development can reduce faults and costs. Modelling languages for design have been shown through practical experience to improve communication through better information presentation and increased information consistency. In this paper, we describe a SysML profile designed for modelling the safety-related concerns of a system. The profile models common safety concepts from safety standards and safety analysis techniques integrated with system design information. We demonstrate that the profile is capable of modelling the concepts through examples. We also show the use of supporting tools to aid the application of the profile through analysis of the model and generation of reports presenting safety information in formats appropriate to the target reader. Through increased traceability and integration, the profile allows for greater consistency between safety information and system design information and can aid in communicating that information to stakeholders.     

A linguistic-engineering approach to large-scale requirements management

For large software companies, the sheer number of textual requirements presents specific challenges. To find market opportunities, organizations must continuously elicit new requirements and reevaluate old ones as market needs evolve. Developing large, complex software products aimed at broad markets involves identifying and maintaining the link between product requirements and the massive inflow of customers' wishes. Automating this support through linguistic engineering could save considerable time and improve software quality.     

How to combine inconsistent ordinal and cardinal preferences: A satisficing modelling approach

This paper analyzes a situation where a decision-maker provides cardinal and ordinal information about her/his preferences towards m objects (criteria, alternatives, etc.). However, the two rankings derived from her/his preferences are different. This situation of “inconsistent preferences” is formalized. Moreover, in order to deal with this type of conflictive situation, a satisficing model based on the minimization of p-metric distance functions is proposed. In this way, a final set of weights associated with the m objects, by using the cardinal and the ordinal information, is obtained. The final model corresponds to a linear extended goal programming, so the proposed approach is operationally and computationally efficient, since the computations are reduced to solving a small number of linear programming models of a moderate size.