China
Africa
Explore chapters and articles related to this topic
Data Mining – Unsupervised Learning
Published in Rakesh M. Verma, David J. Marchette, Cybersecurity Analytics, 2019
Rakesh M. Verma, David J. Marchette
In [500], researchers have presented a method for malware detection based on association rule mining. The hypothesis of their technique, as well as a lot of work on malware detection, is that malware exhibits its behavior through system calls. The unfortunate fact is that we can reduce the halting problem for Turing machines to the problem of determining a program’s behavior, so the latter problem is also undecidable. However, we can still estimate program behavior, which is the basis for their method and other malware detection techniques.
An ASM-based characterisation of starvation-free systems
Published in International Journal of Parallel, Emergent and Distributed Systems, 2018
Alessandro Bianchi, Sebastiano Pizzutilo, Gennaro Vessio
Concerning automatic analysis, several examples of model checking techniques applied to ASMs exist. In [23] the authors introduce a way to translate ASM specifications into the Symbolic Model Verifier (SMV) language. The goal is to link the workbench they built to the model checker SMV. Another application of model checking techniques to ASMs, based on the CoreASM modeling framework, has been proposed in [24]. In particular, CoreASM-based specifications are transformed into models, written by using the Promela modeling language, that can be verified with the model checker Spin. A tool, AsmetaSMV, that enriches the ASMETA framework with the capabilities of the model checker NuSMV to verify properties of given ASM models is presented in [25]. Moreover, in [26] the authors present an approach to verify ASM models, specified in terms of the Asmeta language, using the model checker Bogor. However, all these solutions present the drawback due to the Turing-completeness of the ASM formalism [17]: properties are, in general, undecidable, so the formal verification of ASM specifications cannot be fully automatised [27]. In fact, an algorithm capable of verifying a specific configuration of a given ASM would be able to verify that a certain configuration, e.g. a halting one, is reachable by a Turing machine expressed by means of an ASM. Since the halting problem for Turing machines is undecidable, such an algorithm cannot exist. For this reason, the translation of the given ASM into the input required by the adopted model checker may cause a loss of expressive power.