Understanding the replication machinery of viruses contributes to suggest and try effective antiviral strategies. Exhaustive knowledge about the proteins structure, their function, or their interaction is one of the preconditions for successfully modeling it. In this context, modeling methods based on a formal representation with a high semantic expressiveness would be relevant to extract proteins and their nucleotide or amino acid sequences as an element from the replication process. Consequently, our approach relies on the use of semantic technologies to design the SARS-CoV-2 replication machinery. This provides the ability to infer new knowledge related to each step of the virus replication. More specifically, we developed an ontology-based approach enriched with reasoning process of a complete replication machinery process for SARS-CoV-2. We present in this paper a partial overview of our ontology OntoRepliCov to describe one step of this process, namely, the continuous translation or protein synthesis, through classes, properties, axioms, and SWRL (Semantic Web Rule Language) rules.

Efficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. Discrete-Time approaches and dense representation of time were successfully introduced in SPIN as extensions but suffer of the expected statespace explosion problem. Another approach using discrete-event representation of time and simulation has been proposed to minimize this statespace explosion problem. In this paper, we show how this extension, DEv-PROMELA, can be used in order to model and verify software designs by combining simulation and formal verification.

Abstract Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no support for them. In this paper we propose to add partial functions as a primitive feature to a Constraint Logic Programming (CLP) language, namely {log}. Although partial functions could be programmed on top of {log}, providing them as first-class citizens adds valuable flexibility and generality to the form of set-theoretic formulas that the language can safely deal with. In particular, the paper shows how the {log} constraint solver is naturally extended in order to accommodate for the new primitive constraints dealing with partial functions. Efficiency of the new version is empirically assessed by running a number of non-trivial set-theoretical goals involving partial functions, obtained from specifications written in Z.

Verification and Validation (V&V) of Systems is an important process in the development of systems, in order to ensure that they are reliable and operational. Among methods of V&V, there are two that seem to be opposite to each other: simulation, which is empirical, and formal verification, which is comprehensive. Moreover, simulation and formal verification propose many different formalisms, increasing the gap between them. But, jointly used, these two powerful tools allow making a more efficient verification, increasing the confidence we can put in the verified systems. The main problem is how we can combine their use and how we can reduce the gap created by the nature of both of them. This paper presents guidelines and a general approach in order to use simulation, and especially discrete-event simulation, on a model specified in a verifiable formal language.

This paper describes tool support that has been implemented for the Test Template Framework (TTF). The TTF is a model-based testing (MBT) method that is especially well suited for unit testing from Z specifications. Although the TTF is a sound MBT method and it has been widely referenced since its first publication, attention in recent years has decayed. In fact, some have argued that generating abstract test cases following the TTF is a manual task requiring its users to perform complex predicate manipulations. This paper shows that these observations are dubious by describing Fastest, a tool that implements solutions for all these issues and, according to many experiments, produces abstract test cases for more than 80% of the satisfiable test specifications. Furthermore, it is claimed that Fastest fulfils the needs of the Z user community regarding MBT tools, which is supported with a range of case studies. Copyright © 2012 John Wiley & Sons, Ltd.

This paper put forwards how to improve the collaborative work of company engineers for the control of a manufacturing process. Sharing and using same manufacturing information in industries -such as control indicators- is necessary to efficiently ensure the control task. However, the generalization of Commercial Off-The-Shelf (COTS) systems in manufacturing companies to get such indicators has rapidly entailed the increase of the quantity of the digital resources, where a resource represents manufacturing data presented in specific formats. Retrieving such resources may become impossible without a semantic support. Our solution provides a semantic framework to enhance the retrieval of manufacturing information through the use of a business ontology and a domain-specific dictionary. The specificity of this business semantics is that it brings the resources closer to the business needs on one hand, and it unifies the business vocabulary in the company on other hand.

In this paper we highlight techniques from software engineering to design and code the behaviors of object. After a review of behavioral design patterns, we propose the state event design pattern to design basic behaviors described with state machines. In this pattern we objectify events in addition to states. Then, we generalize this pattern to DEVS behaviors. Thus, the DEVS designers may take profit from this technique to design simulations.

Modeling manufacturing process of complex products like electronic chips is crucial to maximize the quality of the production. This paper proposes a new methodology to model large scale manufacturing processes based on activity information as well as experts' knowledge. DEVS formalism is used for the final models because of its advantages as a formal formalism. This methodology helps to easily detect discrepancies between the actual implementation of processes with experts' definitions. It also helps to construct general models that could be used later for controlling processes. The idea of STMicroelectronics enterprise is to use these general models to implement an alarm system. The idea is to alert engineers about risky modifications done over STMicroelectronics manufacturing processes. The state of our work towards to model STMicroelectronics' production processes is presented at the end of this paper.

We have applied Fastest, an implementation of the Test Template Framework, to five real case studies of aerospace software. This involved the formalization in the Z notation of nontrivial parts of each system. One of these models, for instance, formalizes a significant portion of the ECSS-E-70-41A aerospace standard. The models were then fed into Fastest, which automatically generated detailed functional abstract test cases. Since these test cases are independent of any implementation, they can be used to test any of them. Furthermore, we were able to semi-automatically translate them into English so they can be used by domain experts performing independent validation and verification activities.

In this paper, we present an improvement to evaluate the HLA lookahead for distributed DEVS/G-DEVS models in a HLA-compliant environment. The models considered in this distributed simulation have state lifetimes functions of several state variables. We use the graph theory Dijkstra search to compute the different values of the state variables and a mathematical function analysis to determine the lookahead for the model states. We illustrate on an example how this solution extends the range of DEVS/G-DEVS models that can be involved into distributed simulations.

In this paper we present a method for building a knowledge based system for computer aided diagnosis. This method concerns specification, operationalization and validation of expert knowledge. First, it consists in defining an acquisition model adapted to this kind of knowledge in terms of extended event graphs. Then the model is operationalized by using the DEVS formalism. The obtained model can be used for computer aided diagnosis or control.

the object of the system presented in this article is to allow experienced designers to describe their knowledge in the way to chain a group of CAD software to resolve a given problem and this, in the form of production rules. This system establish a clear separation between the competencies of the computer scientist, the experienced designer and the final user. It permits the procedure bank of be CAD system to the considered as a group of basic elements from which chaining scenario adapted to the different design problems can be described so as to guide the final user.