We propose a novel framework for adapting and evolving software requirements models. The framework uses model checking and machine learning techniques for verifying properties and evolving model descriptions. The paper offers two novel contributions and a preliminary evaluation and application of the ideas presented. First, the framework is capable of coping with errors in the specification process so that performance degrades gracefully. Second, the framework can also be used to re-engineer a model from examples only, when an initial model is not available. We provide a preliminary evaluation of our framework by applying it to a Pump System case study, and integrate our prototype tool with the NuSMV model checker. We show how the tool integrates verification and evolution of abstract models, and also how it is capable of re-engineering partial models given examples from an existing system.

The effective integration of knowledge representation, reasoning, and learning in a robust computational model is one of the key challenges of computer science and artificial intelligence. In particular, temporal knowledge and models have been fundamental in describing the behavior of computational systems. However, knowledge acquisition of correct descriptions of a system's desired behavior is a complex task. In this paper, we present a novel neural-computation model capable of representing and learning temporal knowledge in recurrent networks. The model works in an integrated fashion. It enables the effective representation of temporal knowledge, the adaptation of temporal models given a set of desirable system properties, and effective learning from examples, which in turn can lead to temporal knowledge extraction from the corresponding trained networks. The model is sound from a theoretical standpoint, but it has also been tested on a case study in the area of model verification and adaptation. The results contained in this paper indicate that model verification and learning can be integrated within the neural computation paradigm, contributing to the development of predictive temporal knowledge-based systems and offering interpretable results that allow system researchers and engineers to improve their models and specifications. The model has been implemented and is available as part of a neural-symbolic computational toolkit.

In software development, formal verification plays an important role in improving the quality and safety of products and processes. Model checking is a successful approach to verification, used both in academic research and industrial applications. One important improvement regarding utilization of model checking is the development of automated processes to evolve models according to information obtained from verification. In this paper, we propose a new framework that make use of artificial intelligence and machine learning to generate and evolve models from partial descriptions and examples created by the model checking process. This was implemented as a tool that is integrated with a model checker. Our work extends model checking to be applicable when initial description of a system is not available, through observation of actual behaviour of this system. The framework is capable of integrated verification and evolution of abstract models, but also of reengineering partial models of a system.

The integration of logic-based inference systems and connectionist learning architectures may lead to the construction of semantically sound cognitive models in artificial intelligence. The use of hybrid systems has shown promising results as regards the computation and learning of classical reasoning within neural networks. However, there still remains a number of open research issues on the integration of non-classical logics and neural networks. We present a new model for integrating symbolic reasoning about past temporal information and neural learning systems. We propose algorithms that translate background knowledge into a neural network and analyse the effectiveness of learning algorithms when subject to symbolic temporal knowledge. This opens several interesting research paths with possible applications to agents' decision making, cognitive modelling and knowledge-based systems.