The validation of formal specifications is a challenging task. It is one of the factors that
impede the penetration of formal methods into the common practices of software …

Traces are used to show whether a model complies with the intended behavior. A modeler
can use trace checking to ensure the preservation of the model behavior during the …

A significant impediment to the uptake of formal refinement-based methods among
practitioners is the challenge of validating that the formal specifications of these methods …

Advanced medical devices exploit the advantages of embedded software whose
development is subject to compliance with stringent requirements of standardization and …

Refinement guarantees that the concrete version of a model does not violate the constraints
introduced at the abstract level. The peculiarity of refinement, however, is that we have no …

Modern production, logistic and assembly systems comprise of a considerable number of
processes which operate by using diverse types of resources. Conceptual design of these …

As real-time systems become more prevalent, there is a need to guarantee that these
increasingly complex systems perform as designed. One technique involves a static analysis …

Advanced medical devices exploit the advantages of embedded software whose
development, due to their direct impact on human lives, is naturally subject to compliance …

Refinement-based formal methods provide a systematic process to develop software that is
correct by construction through a gradual enrichment of models. However, their waterfall-like …

A state traversal algorithm based on control theory and its application to sequential ATPG is
presented. In the algorithm, next states are evaluated by an objective function representing“ …