A systematic mapping of semi-formal and formal methods in requirements engineering of industrial Cyber-Physical systems

Journal of Intelligent Manufacturing - The requirements engineering of Industrial Cyber-Physical Systems is extremely challenging due to large system sizes, component heterogeneity, involvement of...     

Local Module Checking for CTL Specifications

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also known as reactive systems) where the nondeterminism in the environment must be considered during verification. Module checking is an approach for the verification of open systems which have both closed (internal) and open (environment or external) states. It has been demonstrated in [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164:322–344, 2001] that the complexity of module checking branching time logic CTL is EXPTIME-complete. The approach to module checking is global and the method tries to establish that the property in question holds over all possible environments.This papers develops a local approach to CTL module checking using tableau rules. The proposed approach tries to determine a single environment under which the negation of the property is satisfied over the given module. Such a strategy, thus, leads to a local approach to module checking where we only explore states that are relevant to proving that the negation of the property can be satisfied over the given module using an appropriate witness (environment) that the algorithm also generates. While the worst case complexity of our algorithm is identical to the earlier complexity, we demonstrate that practical implementation of the proposed approach is feasible and yields much better results than the global approach.     

Angularly continuous light‐field format: Concept,implementation, and evaluation

In this paper, we present the concept, the implementation, and the evaluation of our novel angularly continuous light‐field format. We compared the subjective visual performance of our format with the perspective camera format through a series of subjective and objective tests. In our extensive subjective study, we used multiple absolute and comparative rating scales and various visual stimuli with different contents and angular resolutions. The perceived quality was assessed by a total of 36 test participants, who were separated based on their scientific expertise. The objective quality was evaluated through the degradations caused by three well‐known compression methods. The obtained results indicate that our light‐field format may outperform the conventional format, and it generally can provide at least equivalent visual quality. Furthermore, these findings open the way for data size optimization, without compromising the achieved level of perceived quality.     

FLASc: a formal algebra for labeled property graph schema

Automated Software Engineering - Mailing lists are a major communication channel for supporting developer coordination in open-source software projects. In a recent study, researchers explored...     

Adaptive Verification using Forced Simulation

Simulation (a pre-order) over Kripke structures is a well known formal verification technique. Simulation guarantees that all behaviours of an abstracted structure (a property or function, F) are contained in a larger structure (a model M). A model, however, may not always simulate a property due to the presence of design errors. In this case, the model is debugged manually. In this paper, we propose a weaker simulation over structures called forced simulation for automated debugging. Forced simulation is applied when normal simulation fails. Forced simulation between a model (M) and a function (F) guarantees the existence of a modifier, D, to adapt M so that the composition of M and D is observationally equivalent to F. Observational equivalence over structures called weak bisimulation is developed in this paper. It is also established that when two structures are weakly bisimilar all CTL^* properties holding over one also holds over the other structure. Forced simulation based algorithm has been used to adapt many designs which had failed certain properties during conventional verification.     

Tracing security requirements in industrial control systems using graph databases

Software and Systems Modeling - We must explicitly capture relationships and hierarchies between the multitude of system and security standards requirements. Current security requirements...