Although deep learning models have shown promising results in solving problems related to image recognition or natural language processing, they do not match how the biological brain works. Some of the differences include the amount of energy consumed, the way neurons communicate, or the way they learn. To close the gap between artificial neural networks and biological ones, researchers proposed the spiking neural network. Layered Spiking Neural P systems (LSN P systems) are networks of spiking neurons used to solve various classification problems. In this paper, we study the LSN P systems in the context of a federated learning client-server architecture over horizontally partitioned data. We analyze the privacy implications of pre-trained LSN P systems through membership inference attacks. We also perform experiments to assess the performance of an LSN P system trained in the federated learning setup. Our findings suggest that LSN P systems demonstrate higher accuracy and faster convergence compared to federated algorithms based on either perceptron or spiking neural networks.

Kernel P systems have been introduced as a unifying formalism allowing to specify, simulate and analyse various problems. Several applications of this model have been considered and a powerful tool built in order to support their development and analysis. Testing represents an important aspect of any system analysis and correctness. In this paper we introduce for the first time a bounded test generation approach for kernel P systems by considering bounded input sequences. A learning algorithm for kernel P systems is based on learning X-machine models that are equivalent to these systems for sequences of steps up to a certain limit, ℓ. The Lℓ learning algorithm is used. The testing approach is then devised from the inferred X-machines. The method is applied to a case study illustrating the key parts of the approach.

We present a binary analysis framework based on symbolic execution with the distinguishing capability to execute stepwise forward and also backward through the execution tree. It was developed internally at Bitdefender and code-named RIVER. The framework provides components such as a taint engine, a dynamic symbolic execution engine, and integration with Z3 for constraint solving. In this paper we will provide details on the framework and give an example of analysis on binary code.

Abstract One of the great benefits of using a stream X-machine to specify a system is its associated testing method . Under certain design for test conditions , this method produces a test suite that can determine the correctness of the implementation under test ( IUT ), provided that the basic components of the stream X-machine model have been correctly implemented. However, such an approach implies that each component can be tested in isolation from the rest of the system. This is a limitation that, in practice, can be resolved by developing stubs and drivers. However, this adds complexity to the testing process and, furthermore, these new pieces of software can introduce faults that can invalidate the theoretical results of the aforementioned testing method. This paper extends the approach by allowing component testing to be performed in parallel with integration testing, while still guaranteeing the IUT correctness under the given design for test conditions. It also shows how the integration test suite, produced in previous publications, can be reduced.

We propose an approach which, given a state-transition model of a system, constructs, in parallel, an approximate automaton model and a test suite for the system. The approximate model construction relies on a variant of Angluin's automata learning algorithm, adapted to finite cover automata. A finite cover automaton represents an approximation of the system that only considers sequences of length up to an established upper bound ℓ. Crucially, the size of the cover automaton, which normally depends on ℓ, can be significantly lower than the size of the exact automaton model. Thus, controlling ℓ, the state explosion problem normally associated with constructing and checking state-based models can be mitigated. The proposed approach also allows for a gradual construction of the model and of the associated test suite, with complexity and time savings. Moreover, we provide automation of counterexample search, by a combination of black-box and random testing, and metrics to evaluate the quality of the produced results. The approach is presented and implemented in the context of the Event-B modeling language, but its underlying ideas and principles are much more general and can be applied to any system whose behavior can be suitably described by a state-transition model.

As unconventional computation matures and non-standard programming frameworks are demonstrated, the need for formal verification will become more prevalent. This is so because “programming” in unconventional substrates is difficult. In this paper we

State-based languages are widely used for modelling systems that have an internal state, such as communications protocols and embedded control systems. As testing is a vital part of system development, this has led to much interest in testing from finite state machines (FSMs). However, complex systems are seldom designed in one step; usually, the design is constructed gradually, through a process of refinement. In the case of state-based models, this may lead to a hierarchy of machines. Furthermore, some of the components of the hierarchy may exhibit concurrent behaviour. In this paper, we present a method for generating tests for a hierarchical FSM by reusing and refining the tests for the FSM components of the hierarchy. The method is also adapted for testing a system of communicating FSMs, in which the communication is one-directional, from one master to one or more slaves.

The application of metaheuristic search techniques in test data generation has been extensively investigated in recent years. Most studies, however, have concentrated on the application of such techniques in structural testing. The use of search-based techniques in functional testing is less frequent, the main cause being the implicit nature of the specification. This paper investigates the use of search-based techniques for functional testing, having the specification in form of a state machine. Its purpose is to generate input data for chosen paths in a state machine, so that the parameter values provided to the methods satisfy the corresponding guards and trigger the desired transitions. A general form of a fitness function for an individual path is presented and this approach is empirically evaluated using three search techniques: simulated annealing, genetic algorithms and particle swarm optimization.

Abstract A stream X-machine (SXM) is a type of extended finite state machine with an associated development approach that consists of building a system from a set of trusted components. One of the great benefits of using SXMs for the purpose of specification is the existence of test generation techniques that produce test suites that are guaranteed to determine correctness as long as certain well-defined conditions hold. One of the conditions that is traditionally assumed to hold is controllability: this insists that all paths through the SXM are feasible. This restrictive condition has recently been weakened for testing from a deterministic SXM. This paper shows how controllability can be replaced by a weaker condition when testing a deterministic system against a non-deterministic SXM. This paper therefore develops a new, more general, test generation algorithm for testing from a non-deterministic SXM.

Abstract The X-machine testing method has been developed as an application of the W-method to testing the control structure of an implementation, against a specification. The method was proven to demonstrate the equivalence of the behaviour of the two, subject to a number of conditions both a specification and an implementation are expected to satisfy, such as (1) determinism of the two and (2) that functions labelling arcs on a transition diagram of a specification control structure have been tested in advance. Since the original publication of the testing method, a number of extensions have been published, removing the restrictions mentioned above. This paper surveys the extensions of the X-machine testing method, for (1) testing of functions together with testing of a transition diagram, (2) equivalence testing of a non-deterministic implementation against a non-deterministic specification, (3) conformance testing of a deterministic implementation against a non-deterministic specification and (4) equivalence testing of a system of concurrently executing and communicating X-machines, against a specification.

A cover automaton of a finite language L is a finite automaton that accepts all words in L and possibly other words that are longer than any word in L. An algorithm for constructing a minimal cover automaton of a finite language L is given in a recent paper. This paper goes a step further by proposing a procedure for constructing all minimal cover automata of a given finite language L. The concept of cover automaton is then generalized to a form of extended finite automaton, the stream X-machine, and the procedure is extended to this more general model.

Abstract. One of the strengths of using stream X-machines to specify a system is that, under certain well defined conditions, it is possible to produce a test set that is guaranteed to determine the correctness of an implementation. However, the existing method assumes that the implementation of each processing function is proved to be correct before the actual testing can take place, so it only test the system integration . This paper presents a new method for generating test sets from a deterministic stream X-machine specification that generalises the existing integration testing method. This method no longer requires the implementations of the processing functions to be proved correct prior to the actual testing. Instead, the testing of the processing functions is performed along with the integration testing.

One approach to formally specifying a system is to use a form of extended finite-state machine called a stream X-machine. A stream X-machine is a type of X-machine that describes a system as a finite set of states, each with an internal store, called memory, and a number of transitions between the states. A stream X-machine may be modelled by a finite automaton (the associated finite automaton) in which the arcs are labelled by function names (the processing functions). One important problem that may appear in the specification process is to find a ‘minimal’ (in some sense) stream X-machine that specifies the required functionality. This paper investigates the minimality issue in the context of deterministic stream X-machines and considers two types of minimality: state-minimal stream X-machine with respect to $\Phi$ and minimal cover with respect to $\Phi$, where $\Phi$ is the set of processing functions that the machine may use.

Abstract. X-machines were proposed by Holcombe as a possible specification language and since then a number of further investigations have demonstrated that the model is intuitive and easy to use. In particular, stream X-machines ( SXM ), a particular class of X-machines, have been found to be extremely useful in practice. Furthermore, a method of testing systems specified as SXMs exists and is proved to detect all faults of the implementation provided that the system meets certain “design for test conditions” . Recently, a system of communicating SXMs was introduced as a means of modelling parallel processing. This paper proves that each communicating machine component can be transformed in a straightforward manner so that the entire system will behave like a single stream X-machine - the equivalent SXM of the system. The paper goes on to investigate the applicability of the SXM testing method to a system of communicating SXMs and identifies a class of communicating SXMs for which the equivalent SXM of the system meets the “design for test conditions”.

Abstract. X-machines were proposed by Holcombe as a possible specification language and since then a number of further investigations have demonstrated that the model is intuitive and easy to use as well as general enough to cater for a wide range of applications. In particular (generalised) stream X-machines have been found to be extremely useful as a specification method and most of the theory developed so far has concentrated on this particular class of X-machines. Furthermore, a method for testing systems specified by stream X-machines exists and is proved to detect all faults of the implementation provided that the system meets certain initial requirements. However, this method can only be used to generate test sequences from deterministic X-machine specifications. In this paper we present the theoretical basis for a method for generating test sets from non-deterministic generalised stream X-machines.

Although testing is a major part of software development, it rarely gets the attention it deserves from researchers, partly because its foundations are weak and ill-understood. The principal purpose of testing is to detect (and then remove) faults in a software system. However, very few of the existing methods allow the tester to make any precise statement about the type or number of faults that remain undetected after testing is completed. In particular, none of the main techniques used by the software industry can give serious guarantees that a system is fault-free after testing has been completed. This paper advocates the use of a formal method both as a specification language and as the basis of a test data selection strategy. It presents a new method for generating test cases from this type of formal specification that provides a more convincing answer to the problem of detecting all faults in a software system. The method is reductionist in the sense that it guarantees that a system is fault-free provided that its components are fault-free; in turn, the same method could be used to test the resulting sub-systems, so the reduction will continue until the components considered are either known to be correct or are fairly simple pieces of code that can be successfully tested using traditional methods. The formal method used, X-machines, is a blend of finite state machines, data structures and processing functions and provides a simple and intuitive way of specifying computer systems. The use of X-machines as a specification tool and the testing method are illustrated with a case study. © 1998 John Wiley & Sons, Ltd.