Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula φ, of size at most O(3 |φ |), where |φ | is the length of φ. This result improves upon the previously known bound of O(5|φ |) for rLTL verification and is closer to the LTL bound of O(2|φ |). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.

A Framework for Model and Verification of Safety-Critical Operating System Based on ARINC653

As the scale and complexity of safety-critical software continue to grow, it is necessary to ensure safety and reliability to avoid minor errors leading to catastrophic disasters. Meantime, the traditional method, such as testing and simulation alone is insufficient to ensure the correctness of systems. This leads to using formal methods to provide sufficient evidence for systems. However, design a high assurance safety-critical system by formal methods is challenging due to the complexity of operating systems. In addition, the traditional interactive theorem prover used in system verification requires hand-written proofs, which are more expensive. Therefore, the efforts of providing a standardized formal framework as well as safety proofs, are notable for the develop a safety-critical system. The purpose of this paper is to provide a safety framework to establish a highly reliable and safety-critical operating system based on the ARINC653 standard, a multilevel and standardized formal model. To verify the functional correctness of this model, we propose a context-based formal proof method for programs. To achieve this goal, we first model 57 core services of ARINC653 and define the high-level requirements as pre-and post-conditions. Then, we construct a set of specification statements a formal axiom system transformed into logical sentences, and the core service model is transformed into a logical sentence sequence to be proved. Finally, a context-based formal proof system for specification correctness is developed. We have verified the correctness of safety-critical operating system core services with this system. Experience shows that the verification system we developed can be achieved the functional correctness of a complete OS with a low implement burden, and that can simplify the difficulty of automated verification and increase the degree of automation of proof.

Industrial solar collector vs alternative solar collector: Environmental impact comparison by LCA perspective / Colector solar industrial versus colector solar alternativo: Comparação do impacto ambiental por perspectiva LCA

Adequacy to sustainable development standards requires the use of methods and tools that enable the quantification and monitoring of environmental impacts related to production processes. As a subsidy to the potential reduction of impacts by solar collectors, this paper proposes an environmental evaluation, considering an alternative solar collector scenario to be compared with a commercial one, from the life cycle perspective. Using the Life Cycle Assessment (LCA) tool, the scenarios were evaluated using the SimaPro 8.5 software. The functional unit definition was defined with real system verification through the system preparation and operation in the laboratory, which is characterized as heating 26 L of water utilizing a thermosyphon system at a temperature greater than or equal to 38 ºC. Analyzing the LCA results, it was observed that the alternative system use offers environmental impacts reduction in all impact categories selected when compared to the commercial system. In addition, a sensitivity analysis was proposed considering a variation in polyester resin mass used in the alternative system. The simulation of changes in the resin resulted in even more decreases in the environmental impacts. Regarding thermal efficiency, the industrial system excelled in terms of absorption capacity and thermal reserve. Thus, the present paper using the analyzes proposed within the defined scope, allowed the comparison between the systems in such a way that it was possible to know whether the use of the alternative solar collector results in environmental advantages without losing thermal efficiency.