1,721,011 research outputs found
Verifying Embedded C Software with Timing Constraints using an Untimed Bounded Model Checker
No full textEmbedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We describe an approach to specify discrete-time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checkers such as ESBMC. Moreover, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood
Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
No full textEmbedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood
Applying Scrum and Organizational Patterns to Multi-site Software Development
No full textThis paper describes a pattern language for managing multi-site software projects which aims at minimizing the main problems present on the multi-site software development context. The practices and patterns of the proposed language were first identified from the literature and adapted according to the authors’ experience after running some multi-site software projects. This exercise has led to the identification of two new patterns: "Stories Rework Subsystem", and "Plan Bugs On a Sustainable Pace", as well as to an alternative application of the existing "Inversion of Control" pattern to the organizational context
Towards A Semiformal Development Methodology for Embedded Systems
No full textIn recent days, the amount of functions has increased significantly in embedded products so that systems development methodologies play an important role to ensure the product’s quality, cost, and time. Furthermore, this complexity coupled with constantly evolving specifications, has led to propose a semiformal development methodology to support the building of embedded real-time systems. A platform-based design approach has been used to balance costs and time-to-market in relation to performance and functionality constraints. We performed three expressive case studies and we concluded that the proposed methodology significantly reduces design time and improves software modularity and reliability
A Formal Method for Modeling, Verification and Synthesis of Embedded Reactive Systems
No full textEmbedded reactive systems are now invisible and everywhere, and are adopted, for instance, to monitor and control critical tasks in cars, airplanes, traffic, and industrial plants. However, the increasing amount of new functionalities being moved to software leads to difficulties in verifying the design correctness. In this context, we propose a novel design method called BARE Model, which is a formal abstraction to design, verify and synthesize software in embedded reactive applications. The method consists in designing the application using an extension of the well-known finite state machine, called X-machine. We thus propose to translate this model to a tabular data structure, which is a kind of state transition table augmented with memory input, memory output, and condition (or guard). This tabular structure may be automatically translated to the input of the NuSMV model checker in order to verify the system’s properties. We also propose a runtime environment to execute the system (expressed as a tabular data structure) in a specific platform. In this way, we can convert the high-level specification into executable code that runs on a target platform. To show the practical usability of our proposed method, we experimented it with the Envirotrack case study. The experiment shows that the proposed method is able to not only model the system, but also to verify safety and liveness properties, and synthesize executable code of real-world applications
Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs
No full textThe use of computer-based systems in several domains such as automotive, industrial automation, and transportation has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. The value of the counterexample and safety properties generated by Bounded Model Checkers to create test case and to debug these systems is highly recognized. In this paper, we describe a method to integrate the bounded model checker ESBMC with the CUnit framework. This method aims to extract the safety properties generated by ESBMC to generate automatically test cases using the rich set of assertions provided by the CUnit framework. We show the effectiveness of our proposed method over publicly available benchmarks
Towards a Model-Driven Engineering Approach for Developing Embedded Hard Real-Time Software
No full textModel-Driven Engineering (MDE) has been advocated as an effective way to deal with today's software complexity. MDE can be seen as an integrative approach combining existing techniques such as Domain-Specific Modeling Languages (DSML) and Transformation Engines. This paper presents the ezRealtime, an MDE-based tool that relies on the Time Petri Net (TPN) formalism and defines a DSML to provide an easy-to-use environment for specifying Embedded Hard Real-Time (EHRT) systems and for synthesizing timely and predictable scheduled C code. The ezRealtime adopts the universal XML-based transfer syntax for Petri nets, named as PNML. The main idea of this work is to propose a generative programming method and tool to boost code quality and improve developer productivity with automated software synthesis. The ezRealtime tool reads and automatically translates the specification to a time Petri net model through composition of building blocks with the purpose of providing a complete model of all tasks in the system. Therefore, this model is used to find a feasible schedule by applying a depth-first search algorithm. Finally, the scheduled code is generated by traversing the feasible schedule, and replacing transition's instances by the respective code segments. We also present the application of the proposed method in a case study
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
An Agile Development Methodology Applied to Embedded Control Software under Stringent Hardware Constraints
No full textIn recent years, discrete control systems play an important role in the development and advancement of modern civilization and technology. Practically every aspect of our life is affected by some type of control systems. This kind of system maybe classified as an embedded real-time system and requires rigorous methodologies to develop the software that is under stringent hardware constraints. Therefore, the proposed development methodology adapts agile principles and patterns in order to build embedded control systems focusing on the issues related to the system's constraints and safety. Strong unit testing is the foundation of the proposed methodology for ensuring timeliness and correctness. Moreover, platform-based design approach is used to balance costs and time-to-market in view of performance and functionality constraints. We conclude that the proposed methodology reduces significantly the design time and cost as well as leads to better software modularity and reliability
- …
