Model Checking is currently one of the most exciting techniques to improve quality complex software systems.It a computer aided verification method that, in many cases, has discovered design bugs early development steps, thus saving time and costs produce final code.Although this technique successfully applied formal description techniques, it not commonly used by object oriented programming community, general, nor UML developers, particular.In paper, we provide comprehensive overview rules...

The behavior of mobile devices is highly non deterministic and barely predictable due to the interaction user with its applications. In consequence, analyzing correctness applications running on a smartphone involves dealing complexity environment. this paper, we propose use model-based testing describe potential behaviors users interacting These are modeled by composing specially-designed state machines. composed machines can be exhaustively explored using model checking tool automatically...

Abstract Software model checking consists in applying the most powerful results formal verification research to programming languages such as C. One general technique implement this approach is producing a reduced of software order employ existing and efficient tools, SPIN . This paper focusses on application avionics constructed top Application Executive ( APEX ) Interface, which widely employed by manufacturers industry. It presents method automatically extract PROMELA models from C source...

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking runtime monitoring. Runtime monitoring is used to transform execution traces into input checker, purpose which twofold. First, it checks these against properties written in linear temporal logic (LTL), represent desirable or undesirable behaviors. Second, produces several a single program by generating test inputs exploring different schedulings multithreaded...

This paper presents the foundations and real use of a tool to automatically detect anomalies in Internet traffic produced by mobile applications. In particular, our MVE is focused on analyzing impact that user interactions have received smartphones. To make analysis exhaustive with regard potential behaviors, we follow model-based approach generate test cases be executed addition, specification language define patterns compared actual device. also includes monitoring verification support...

The need to increase mobility and remove cables in industrial environments is pushing 5G as a valuable communication system connect traditional deterministic Ethernet-based devices. One alternative the adoption of Time Sensitive Networking (TSN) standards over Non-Public Networks (5G NPN) deployed company premises. This scenario presents several challenges, most relevant being configuration part provide latency, reliability throughput balance suitable ensure that all TSN traffic can be...

The aim of IEEE Time-Sensitive Networking (TSN) standards is to grant deterministic communication in traditional Ethernet networks for Industry 4.0. Insofar as the use cases Factory need some mobility, extension TSN capabilities over fifth-generation (5G) cellular network next step. Some challenges 5G, such translators time synchronization functionality, are well defined standards, even if they have not yet been addressed market. However other challenges, dynamic configuration entire (or...

Abstraction methods have become one of the most interesting topics in automatic verification software systems because they can reduce state space to be explored and allow model checking more complex systems. Nevertheless, there is a lack tools actually supporting this technique. One direction for abstracting system transform its formal description (its model) into simpler version specified same language, thus skipping construction specific (model checking) tool abstract model. The...

The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due the presence complex data structures. One recent and promising approach deal with construction an abstract correct representation global program allowing match visited states during exploration. In particular, one powerful method implement <i xmlns:mml="http://www.w3.org/1998/Math/MathML"...