Throughout the history of software, evolution has occurred in cycles of rise and fall driven by competition, and open-source software (OSS) is no exception. This cycle is accelerating, particularly in rapidly evolving domains such as web development and deep learning. However, the impact of competitive relationships among OSS projects on their survival remains unclear, and there are risks of losing a competitive edge to rivals. To address this, this study proposes a new automated method called “Mutual Impact Analysis of OSS (MIAO)” to quantify these competitive relationships. The proposed method employs a structural vector autoregressive model and impulse response functions, normally used in macroeconomic analysis, to analyze the interactions among OSS projects. In an empirical analysis involving mining and analyzing 187 OSS project groups, MIAO identified projects that were forced to cease development owing to competitive influences with up to 81% accuracy, and the resulting features supported predictive experiments that anticipate cessation one year ahead with up to 77% accuracy. This suggests that MIAO could be a valuable tool for OSS project maintainers to understand the dynamics of OSS ecosystems and predict the rise and fall of OSS projects.

As NAND flash memory has become a widely used storage medium, traditional file systems face challenges in adapting to its unique characteristics. The Flash-Friendly File System (F2FS) is designed to optimize file and data management on NAND flash, addressing issues such as raw NAND interface compatibility, the "wandering tree" problem, high reading costs, and inefficient garbage collection. Through a log-structured foundation and various optimizations, including multi-head logging, node address table (NAT), and reserved in-place updated metadata sections, F2FS achieves enhanced performance, reliability, and prolonged lifespan. This study constructs a multi-head log model based on F2FS and introduces a new hardware-independent metric—Write Amplification Factor (WAF)—to analyze performance. The research demonstrates that separating node and data blocks is more effective in improving garbage collection efficiency than simple hot and cold data segregation.

Ensuring the safety of autonomous driving systems (ADSs) through rigorous verification in simulated environments is crucial before real-world deployment. However, using simulation environments for ADS testing and verification poses several challenges, including specifying various behaviors of traffic participants and collecting comprehensive real-time data to verify the ADS. To address these challenges, we propose a framework for runtime verification of ADSs, focusing on Autoware, a leading ADS. This framework integrates AWSIM-Script, a scripting language for defining traffic scenarios; Runtime Monitor, a tool to record real-time data during the simulation; and AW-Checker, a Linear Temporal Logic-based property checker for verifying safety requirements. Unlike prior research that primarily focuses on generating critical scenarios, we leverage a well-established ADS safety standard from the Japan Automobile Manufacturers Association and adopt its systematic methodology for safety assessment. We conducted a series of experiments focused on nonintersection road geometry to evaluate Autoware's capability in handling different traffic disturbances such as cut-in, cut-out, and deceleration scenarios. The results revealed that, compared to the competent and careful driver model, which represents the minimum safety requirements for ADSs, Autoware failed to prevent collisions in some cases, particularly during high-speed scenarios and fast lateral movements by other vehicles.

This paper investigates the use of simulation-based testing for Autoware, an open-source autonomous driving system, for scenario-based safety analysis. We employed the AWSIM-Labs simulator to evaluate Autoware within specific scenarios derived from the safety analysis. The results show the feasibility of using simulation for safety evaluation based on these scenarios, while also revealing gaps between the scenario-based safety analysis and the simulation outcomes. We also identified key challenges in addressing these gaps for our future research.

Recently, the evolution of deep learning has promoted the application of machine learning (ML) to various systems. However, there are ML systems, such as autonomous vehicles, that cause critical damage when they misclassify. Conversely, there are ML-specific attacks called adversarial attacks based on the characteristics of ML systems. For example, one type of adversarial attack is an evasion attack, which uses minute perturbations called "adversarial examples" to intentionally misclassify classifiers. Therefore, it is necessary to analyze the risk of ML-specific attacks in introducing ML base systems. Unfortunately, there are few methods to analyze evasion attacks. In this study, we propose a quantitative evaluation method for analyzing the risk of evasion attacks using attack trees. The proposed method consists of the extension of the conventional attack tree to analyze evasion attacks and the systematic construction method of the extension. Finally, we conducted experiments on three ML image recognition systems to demonstrate the versatility and effectiveness of our proposed method.

Automated driving systems(ADS) are major trend and the safety of such critical system has become one of the most important research topics. We usually use scenarios in order to define the specifications of ADS. In these scenarios, graphical diagrams are often used to represent abstractly the positioning and behavior of vehicles. However, such diagrams are not suitable for the development of high-reliability systems, because they are informal and may cause discrepancies among different engineers. In this paper, we propose a formal speci-fication language called Bounding Box Specification Language (BBSL) which allows us to write rigorous specifications of ADS. BBSL describe multiple types of objects in a driving environment, such as vehicles and pedestrians, as bounding boxes defined as two-dimensional interval, and describe positional relationships between them in mathematical notation. It is capable of strictly delineating many positional relationships while being also capable of expressing specifications that are concise enough to be read and written manually. Therefore, BBSL is suitable for describing the specification of Object and Event Detection and Response (OEDR) among the tasks of ADS. In this paper, we describe what kind of description BBSL enables, and describe its operations. Then, we show examples of specifications of ADS written in BBSL and discuss the advantages of specifications written in BBSL.

Simulink is a popular tool for modeling cyber-physical systems. As more models are produced in industry, automated quality assurance of models becomes increasingly important. This paper describes an empirical evaluation of four methods for the coverage testing of Simulink models: A) SimuLink Design Verifier (SLDV), a dedicated official tool; B) Template-Based Monte-Carlo (TBMC) method, a random test generation method that utilizes input signal templates; C) SMT- Based Model Checking (SBMC) method that conducts static analysis via encoding models into logic formulas; and D) a hybrid method of B and C. Based on the evaluation results, we carefully designed the hybrid method to complement the features of TBMC and SBMC. In the experiments, we have applied the methods to fourteen models and evaluated their performance. The results show that the hybrid method achieved better results than SLDV for several models.

Summary In existing computer systems, file systems are indispensable for organizing user data and system codes. However, several studies have reported certain file system errors that cause significant data loss or system crashes. Most of these errors are due to external failures, such as an unexpected power outage. However, comprehensively evaluating file system robustness to detect these errors is challenging. The various types of file systems use different data structures and algorithms for various applications. Moreover, file system errors may be triggered by an unpredictable external condition. In addition, a file system works in an operating system's kernel layer as a passive module and runs in a multi‐thread mode, which makes file system testing time‐intensive. Furthermore, the large number of states in file systems leads to greedy checking, which results in a state explosion. In this study, we comprehensively evaluated the robustness expected in multiple properties of file systems using a model checking approach. The evaluation covered the majority of the mainstream file system types and included both single‐thread and multi‐thread modes. We developed Promela models that abstracted the real file systems and subsequently checked them using a SPIN model checker. Our model was optimized to avoid state explosion during model checking. Using the model checking, we successfully detected corner‐case errors during an unexpected power outage. By analysing counterexamples generated by model checking, we determined an improved file system model capable of preventing errors in most mainstream file system types. Finally, we rechecked the improved file system model and verified the absence of all critical errors.

The execution of a software system that runs on top of an Operating System (OS) is usually controlled by the scheduler. Therefore, to accurately verify the system, the scheduling policy needs to be taken into account in the verification. In model checking techniques, the scheduling policy affects the search algorithm to explore the state space to check the behaviors of the system. Existing works try to specify/implement the scheduler(s) along with the set of processes in the specification language(s) used by the model checking tool(s). In reality, many kinds of scheduling policies are used by the OS(s), e.g. round-robin, priority, and first-in-first-out. There are also many variations of these policies, which are usually different from the 'textbook’ ones. That means dealing with the variations of the scheduling policies in model checking is necessary and important. However, because the implementation of the scheduler always starts from scratch, it is error-prone and time-consuming. Therefore, the existing works are difficult to deal with the different scheduling policies. To address this problem, we propose a method that introduces a domain-specific language (DSL) to facilitate the variation of the policies. All necessary information to perform the scheduling tasks is generated automatically from the description of the scheduler. We also introduce a search algorithm using this information to explore the states of the system to verify the behaviors of the system. In this paper, we introduce SSpinJa, a tool in which we implemented this approach. Our tool supports an environment for editing the scheduling policy (in the DSL) and the model checker for verifying the system. The results of our experiments show that a) we can handle different scheduling policies easily, b) we can accurately verify the behaviors of the systems, and c) our approach is also practical.

Summary Handling hardware‐dependent properties at a low level is usually required in developing microcontroller‐based applications. One of these hardware‐dependent properties is cautions, which are described in microcontrollers hardware manuals. The process of verifying these cautions is performed manually, as there is currently no single tool that can directly handle this task. This research aims at automating the verification of these cautions. To obtain the typical cautions of microcontrollers, we investigate two sections which have a considerable number of required cautions in the hardware manual of a popular microcontroller. Subsequently, we analyse these cautions and categorize them into several groups. Based on this analysis, we propose a semi‐automatic approach for verifying the cautions which integrates two static programme analysis techniques (i.e., pattern matching and abstract interpretation). To evaluate our approach, we conducted experiments with generated source code, benchmark source code, and industrial source code. The generated source code, which was created automatically based on several aspects of the C programme, was used to evaluate the performance of the approach based on these aspects. The benchmark and the industrial source code, which were provided by Aisin Software Co., Ltd., were used to assess the feasibility and applicability of the approach. The results show that all expected violations in the benchmark source code were detected. Unexpected but real violations in the benchmark programme were also detected. For the industrial source code, the approach successfully handled and detected most of the expected violations. These results show that the approach is promising in verifying the cautions.

Recently, machine learning, particularly deep learning, is attracting much interest and is applied in various systems. Applications include not only entertainment systems, but safety-critical systems such as those found in autonomous vehicles. The reliability of such safety-critical systems must be guaranteed before they are released into society. However, methods for ensuring the safety of machine learning-based systems have yet to be established. In this paper, we propose a method for systematically evaluating the safety of such systems. The method consists of dataset-based safety analysis and statistical evaluation of testing results. In the safety analysis, we extend the widely used fault tree analysis to deal with datasets. In the testing, we use statistical estimation to guarantee recognition rates obtained in the safety analysis. We conducted experiments using a handwritten character recognition system implemented as a CNN to demonstrate the feasibility and effectiveness of our method.

File systems are used to organize data on storage devices. The file systems may crash due to external failures, such as an unexpected power outage. Therefore, the robustness of the file system is essential. Although some existing works evaluated the robustness of file systems, they are not comprehensive enough and cost many resources. In this work, we design a file system model and verify properties related to the correctness of the file using the SPIN model checker. The robustness of the file system has been comprehensively evaluated in both single-thread and multi-thread modes. There is a critical error in the file system. By analyzing counterexamples given by model checking, we propose a mechanism to prevent it. Based on the mechanism, the robustness of the file system is effectively improved.

Microcontrollers are usually supplied with hardware manuals, where information that requires special attention is emphasized as cautions. Currently, the process of verifying these cautions is performed manually as there is no single tool that can directly handle this task. This research aims at automating the verification process for these cautions as much as possible. Firstly, we investigate two sections which have a considerable number of required cautions in the hardware manual of a popular microcontroller to obtain the typical cautions of microcontrollers. Secondly, we analyze and categorize these cautions into several groups. Subsequently, we propose a semi-automatic approach which uses the assertion-based method and integrates two existing static program analysis tools (i.e., Cobra and Eva plugin of Frama-C) to verify the cautions. To show the applicability of this approach, we conduct two experiments with a benchmark source code and an industrial source code provided by Aisin comCruise Co., Ltd.. The results show that this approach is capable of detecting all violations in the benchmark program and only misses one expected violation in the industrial project.

Static analysis tools have demonstrated their ability to find non-compliant code of coding standards. However, for industrial-sized systems, static analysis tools frequently report a large number of warnings, which contain both true positives and false positives. In this research, to enable precise check for SEI CERT C Coding Standard, we combine static analysis with three different techniques. Firstly, a static analysis tool is used to detect non-compliant code, which are positions that may violate a SEI CERT C rule or recommendation. Each detected position is called a warning. Secondly, deductive verification, model checking, and pattern matching are used to verify whether each warning is a true positive or a false positive. Our experiments with two automotive applications show that this approach can help to improve the accuracy to check for SEI CERT C Coding Standard. We verify nearly 60% warnings of Rosecheckers, a static analysis tool. In these verified warnings, 97% of them are automatically detected to be true positives or false positives by our approach.

MATLAB/Simulink is the de facto standard tool for the model-based development (MBD) of control software for automotive systems. A model developed in MBD is called a Simulink model and, for real automotive systems, involves complex computation as well as tens of thousands of blocks. In this paper, we propose an automated test generation tool for such large and complex Simulink models. The tool provides functions for (1) automatically generating high-coverage test-suites for practical models, which cannot be handled by Simulink Design Verifier (SLDV), and (2) measuring decision, condition and MC/DC coverage much more efficiently than Simulink Coverage (SLC). This automatic test-suite generation adopts a Monte-Carlo method with templates of test cases. Our experimental evaluation shows that the tool can provide test suites against practical implementation models with higher coverage and shorter execution times than SLDV.

Conformance testing is a formal approach for checking the validity of an implemented system against its specification. This paper adopts it to comprehensively check the conformance of smart house temperature with its requirements. However, besides its limited capability to detect thermal problems, e.g., temperature fluctuation, it is inefficient when dealing with thermal problems in different time intervals of a test duration. To overcome these problems, this paper proposes a multiple-conformance approach. We adopt hybrid automata to model the required indoor temperature change as the specification, which enabled the check in different time intervals of the test duration. More conformance rules are prescribed in the multiple-conformance approach to enhance its capability to detect thermal problems. We demonstrate its practical usefulness through an experiment, the results of which demonstrate the effectiveness of the proposed approach in detecting thermal problems.

Hybrid automata are a formal model for dynamical systems with discrete and continuous components. This paper exploits the capability of hybrid automata to model the required indoor temperature change for comprehensively detecting thermal problems. The requirement is to specify the changes in the indoor temperature by considering thermal discomfort that ranges from uncomfortable to serious. We first devise an example of home appliance control service for indoor temperature adjustment. Then, based on the example, this paper proposes the modeling of the required indoor temperature change by hybrid automata. To this end, we represent different states of the hybrid automata, which correspond to different thermal sensations of indoor temperature change, by resorting to various indices. Then, the required indoor temperature change is prescribed by heat exchange between indoor and outdoor. Experiment results demonstrate the capability of hybrid automata to model the required indoor temperature change.

AUTOSAR OS is a standard for automotive operating systems, which provides a specification that consists of functionalities such as scheduling services, timing services, and memory protection. In this paper, we focus on memory protection features among them. As the AUTOSAR OS specification is described in natural language, its ambiguity may confuse developers as well as cause the contradiction of the specification, then eventually lead to serious problems of automotive systems such as bugs and errors. These problems in automotive systems relate directly to the safety of human being. Thus, it is very important to ensure the unambiguity and consistency of the specification. Our solution for the problems is formalizing the AUTOSAR OS specification using Event-B specification language which allows us to formally specify the functionalities of AUTOSAR OS and reduce the ambiguity of natural language. We developed a formal specification of the memory protection of AUTOSAR OS and verified its consistency. In this verification, we found the inconsistency of the specification during discharging proof obligations generated by RODIN which is a tool for Event-B. This inconsistency comes from the ambiguity of the original specification, and finding it by reviewing based on natural language description is very hard. In this paper, we explain how we found the inconsistency existed in the AUTOSAR OS standard after showing our approach to formalize and verify it with Event-B.

In an IVN system, electronic components are connected and communicated through multiple protocols subjected to different requirements. In practice, intelligent vehicles need to exchange data between the body control subsystem and the chassis control subsystem, usually involving both the controller area network (CAN) protocol and the FlexRay protocol. In such a system, delays and congestion of frame transmissions are more likely to happen, leading to safety issues. In this paper, following a two-stage strategy, we managed to find an appropriate abstraction to model the IVN system in the presence of both protocols. Based on the abstraction, we proposed a framework for modeling and verifying IVN systems in their design phase using timed model checking techniques. To analyze the timed properties of communications, we chose the UPPAAL as the platform. Regarding concerns of reusability, this framework was structured in such a way that it is adaptable to IVN systems with different topologies. This framework was validated by checking the communication behaviors against the protocol specifications. We constructed design models with three typical topologies and estimated the response time of frames. The reusability of this framework over different topologies was demonstrated by comparing the estimated response times against the corresponding topological characteristics.

A concurrent system consists of multiple processes that are run simultaneously. The execution orders of these processes are defined by a scheduler. In model checking techniques, the scheduling policy is closely related to a search algorithm that explores all of system states. To ensure the correctness of the system, the scheduling policy needs to be taken into account during the verification. Current approaches, which use fixed strategies, are only capable of limited kinds of policies and are difficult to extend to handle the variations of the schedulers. To address these problems, we propose a method using a domain-specific language (DSL) for the succinct specification of different scheduling policies. Necessary artifacts are automatically generated from the specification of the policy to analyze the system. We also propose a search algorithm for exploring the system states. Based on this method, we develop a tool to verify the system with different scheduling policies. Our experiments show that we could serve the variations of the schedulers easily and verify systems accurately.

A relaxed memory model allows reordering of memory accesses, which can violate program correctness in multiprocessors. This paper presents an approach to verifying a list of assembly programs under a relaxed memory model. Assembly programs are considered for abstractions, which capture essential information that affects the correctness. For program verification, SMT solvers are adopted for finding an execution that violates program property, which is defined by assertions. The solver takes constraints that represent the violation of assertion conditions to find a valuation which can construct an execution. An encoding method is presented for constructing the constraints of program behavior, which classifies the essential behaviors in multiprocessors and can be used by the solvers. An automated tool was developed to abstract the list of assembly programs and find an execution that violates the program assertions. Experiment results show the tool can verify assembly programs for SPARC architecture under SC, TSO, and PSO memory models.

Automotive systems are widely used in industry and our dailylife. As the reliability of automotive systems is becoming a greater challenge in our community, increasingly more automotive companies are interested in applying formal methods to improve the reliability of automotive systems. We focus on automotive operating systems conforming to the OSEK/VDX standard. Such operating systems are considered as important components to ensure the reliability of the automotive systems. Inprevious work, we proposed a framework to verify the design models of reactive systems against their specifications. This framework allows us to check whether the design model conforms to the specification based on a simulation relation. This paper shows a case study in which the framework is applied to a real design of the OSEK/VDX operating system. As aresult, we found that we were able to check several important properties of the design model. We show the effectiveness and practicality of the framework based on the results of the case study.

When a software failure is observed during testing or operation, developers traditionally execute the software program again for reproducing the failure to analyze the cause of the failure. However, failures are often hard to reproduce because they depend on factors that are hard to expressly control, such as concurrency and nondeterminism. This paper presents a novel experimental fault analysis process for such "hard-to-reproduce failures". The proposed process consists of three phases: assumption of a hypothesis for the cause of a failure, experiments to examine the hypothesis and confirmation of the experimental results. We formalized the process and implemented it by using model extraction and model checking. Model extraction acts as a bridge between the assumption and experiment. Experiments on failure reproduction are conducted using model checking. The results of the case studies show that the process and tools supporting the process enables developers to detect the cause of hard-to-reproduce failures in industrial software development.

OSEK/VDX, a standard of automobile OS, has been widely adopted by many manufacturers to design and develop a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more complex applications are developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. As to ensure the reliability of developed applications, model checking as an exhaustive technique can be applied to verify the OSEK/VDX applications. There exist many model checkers that have been successfully applied to verify sequential software and general multi-threaded software. However, it is hard to directly use existing model checkers to precisely verify OSEK/VDX applications, since the execution characteristics of OSEK/VDX applications are different from the sequential software and general multi-threaded software. In this paper, we describe and develop an approach to translate OSEK/VDX applications into sequential programs in order to employ existing model checkers to precisely verify OSEK/VDX applications. The value of our approach is that it can be considered as a front-end translator for enabling existing model checkers to verify OSEK/VDX applications.

Debugging is one of the most time-consuming tasks in software development. The application of a model-checking technique in debugging has strong potential to solve this problem. Here, lessons learned through our practical experiences with POM/MC are discussed. The aim of this proposed hypothesis-based method of debugging is not only to reproduce a failure as counterexamples, but also to obtain a counterexample that is useful for detecting the fault or the cause of the failure. One of the characteristics of the proposed approach is that it degenerates a source code in order to clarify the fault. An example of this degeneration shows that the method is useful for fault analysis and avoidance of the "state-explosion" problem. Furthermore, the characteristics of debugging using POM/MC are explained from the viewpoint of debugging hypotheses.

In practical software development, requirements are usually changed over time due to various reasons. The phenomena of changing requirements are called requirements evolution. It is challenging for requirements engineers to verify and preserve correctness of the requirements in such an evolution. This paper aims to technically analyze the possibility to use a refinement mechanism of Event-B, a formal specification language, to preserve the correctness of requirements in the requirements evolution. By regarding one step of the refinement in Event-B as a step of the evolution, we mathematically prove that the refinement mechanism of Event-B preserves the correctness at every step. This leads to our conclusion that it is possible to use Event-B to help requirements engineers verify and preserve the correctness of requirements during the requirements evolution.

With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.

Formal Methods has been recognized as a rigorous development methodology for hardware and software systems. In particular, model checking is well accepted as an effective verification method for hardware systems, safety/missioncritical systems and embedded systems. To foster this technology in industry, we recognize a need to develop educational materials to enhance learning the technology by students and practitioners. However, there are neither standard guidelines nor instructions how to teach this technology. In this paper, we will present the first draft of a body of knowledge on model checking called MCBOK to address this issue, and present lessons learned from its development experience.

Automotive systems are being standardized by several organizations because they use many parts developed by various companies. Thus, ensuring that those parts conform to standards is very important in this field. Moreover, the automotive systems require high reliability since their bugs or errors may cause serious accidents. In this paper, we focus on operating systems compliant with an OSEK/VDX standard, and propose a method to obtain highly reliable test cases for ensuring the conformance. So far, we have developed a design model based on the standard and made great effort to check that it conforms to the standard with a model checking tool SPIN. Our idea is to use this design model as a test oracle to automatically generate exhaustive test cases with the help of the model checking tool.

In this paper, we propose an alternative approach for verifying a conformance between choreography and the black box implementation of stateful Web service whose only external behaviors can be observed. Our framework uses an adapted version of Angluin's algorithm to infer a Mealy machine model that represents the observable behaviors of the implemented Web service. By transforming the Mealy machine to the modeling formalism LTS, the model checker LTSA can be used for checking a trace equivalence relation which is the conformance criterion in this work.

This paper proposes a different approach for service adaptation which aims to: (i) support non-regular adaptation; (ii) integrate adaptation and model checking. First, a pushdown automaton is used to model the adaptor so that non-regular languages are possible. Second, behavior interfaces of services are modeled by Büchi automata in order to take the advantage of the acceptance condition. By defining the property of ”behavior mismatch free” in a LTL formula using acceptance condition, the detection of behavior mismatches is performed by model checking. Also, the adaptor generation is performed by model checking of pushdown systems with the guidance of a special over-behavioral adaptor called “coordinator”. Then the returned counterexample is converted to a pushdown automaton, the expected adaptor.

In designing real time software, system designers need to find out the time budget to allocate to each action of real time tasks so that the tasks can meet their deadlines. Our solution to this problem involves representing the execution time of the actions as parameters, then analyzing the collaborative behavior of those real time tasks. This paper proposes parametric timed models of real time tasks whose executions are controlled by a scheduler. We develop an algorithm to synthesize a coherent model which represents the possible behavior from a set of real time tasks by exhaustively searching their reachable states. A set of linear inequalities are then derived on the fly from the synthesized model as the condition of parameters for schedulability. By solving the inequalities using a constraint solver, we can obtain desirable values of the parameters. In addition, we have implemented the algorithm in a tool and conducted some experiments to show the effectiveness of our approach.

In this paper, we first reveal an important problem called a state inconsistency problem among tasks based on a design model of a CD/DVD systems.This problem is not only of CD/DVD systems but also of typical embedded software because it may occur in a typical structure that such software has. Thus, we propose a method to detect the problem in the design model with a model checking tool and to derive behavior in which it does not occur.

In this paper, we propose a method to verify software executed on RTOS which conforms to mulTRON with a model checking tool Spin. The RTOS provides facilities such as priorities and service calls to control the execution of tasks, however, Spin does not provide them. Thus, we implemented a middleware which allows us to use the facilities and simulate the execution of the tasks in Spin. The paper shows how it is implemented and its evaluation.

Recently, design models that precise behavior of objects is specified are proposed. Though, currently, they are mainly used for their execution and automatic source code generation, they also have potential to allow us to verify them in the design phase. In this paper, we propose a method to verify such design models in the design phase. In addition, we adopt theorem proving systems to rigorously and efficiently verify it.

In the upstream phase of object-oriented development, we usually model a target system from multiple points of view. A dataflow view has been recognized as one of the most important views in software engineering. We need to relate dataflow models to OO models and check consistency between them as it is still important even if we adopt object-oriented approach. In this paper, we propose a method to analyze dataflows in OO design models with the model checker Spin after formalizing them.

As a result of the increasing size and complexity of embedded systems, object-oriented techniques are going to be adopted in the embedded software development. In embedded software developments, we have to consider non-functional requirements such as real-time properties and resource requirements. To deal with these requirements, some methodologies design the system using a thread-based approach. In such approach, we need to extract threads from the concurrent objects defined in the analysis model. However, current methodologies do not provide enough support to do so. We propose a formal approach to extract threads from concurrent objects. We also present an experimental application of the proposed approach to the development of a device driver.

The scale of software products is becoming larger as a result of the rapid progress and increasing use of computer systems. It is necessary to develop such large-scale software effectively. object-oriented methodologies have been proposed for the development of such systems. In typical object-oriented methodologies like OMT, a target system is described by several model which mirror different views of it. Though it is desirable to analyze models in this style as it enables us to represent independent aspects of the system in orthogonal manner, it causes a difficulty to maintain consistency among them. In this paper, we show a mechanism to unify analysis models at first. This allows us to deal with the models in concepts shared by them. Next we propose a verification method for checking consistency among them with respect to dataflow. In our method, verification is performed by proving dataflow in an axiomatic system.