UML state machine diagrams describe event-driven behavior, but novices struggle to understand how syntactic elements relate to semantics, making learning difficult. Blockbased programming environments such as Scratch, by contrast, are familiar to younger learners and provide an accessible, executable way to explore computational concepts, allowing trial-and-error execution that may ease this understanding. Motivated by this potential, we present a block-based educational tool to support novice learning of state machine representation. Built on Blockly, the tool provides state-machine-oriented blocks that novices can assemble into executable behaviors. To aid comprehension, assembled blocks can be executed with logs and transformed into UML state machine diagrams in PlantUML, linking block assemblies with state machine modeling. In this demonstration, we highlight features that reduce burden for instructors and novices: easy deployment, automatic import of modeling elements (e.g., state names and triggers) defined in JSON as blocks, immediate execution with logs, and diagram generation. As a preliminary evaluation, we surveyed 8 university students with prior exposure to state machine diagrams. While some difficulties arose with specific blocks, no major issues were found. These results suggest that block-based representation may help novices learn state machine concepts more smoothly and support gradual introduction to UML notation. The prototype tool has been released for public access at https://github.com/ 25w6051b/BlockSM, and a demonstration video is also available at https://youtu.be/ZzVBhjWq1zY.

The extraction of non-functional requirements (NFRs) is a crucial yet complex task in information system development, often requiring extensive domain expertise. Traditional persona-driven approaches rely on expert-driven manual processes, which can be inconsistent and inefficient. To address this challenge, we propose an LLM-based autonomous agent framework for persona-driven NFR extraction, integrating Retrieval-Augmented Generation (RAG) to enhance contextual adaptation. The framework systematically automates persona generation, scenario-based experience simulation, interview question formulation, response evaluation, and final NFR specification, incorporating iterative refinement mechanisms. To evaluate its effectiveness, we conducted a case study using a real-world procurement specification, comparing RAG-enabled and non-RAG conditions. Experimental results demonstrate that RAG improves the contextual relevance of interview questions, with an average Context Relevancy Score of 0.5135 compared to 0.4795 without RAG. Additionally, RAG-enabled interviews exhibited broader information coverage in the initial round, as indicated by Convex Hull Volume analysis. However, dynamic flow control mechanisms ensured that non-RAG conditions, through iterative refinement, achieved comparable final NFR completeness. Human evaluation confirmed that the proposed framework generates consistent, structured, and comprehensive NFR specifications while reducing dependency on manual expertise. These findings highlight the potential of integrating LLM agents and RAG to enhance automation and coverage in NFR extraction. Future work will focus on refining adaptive RAG application mechanisms and optimizing persona-driven question generation strategies to further improve the efficiency and accuracy of NFR specification processes.

Common Vulnerability Scoring System (CVSS) is a standard method for quantifying the severity of software vulnerabilities. Security engineers can identify the underlying causes of vulnerabilities and develop countermeasures based on CVSS base vector and their related scores. The CVSS base vector is a set of metrics used to calculate the severity score of a vulnerability based on its intrinsic characteristics, such as “Attack Vector (AV)” and “Privilege Required (PR)‘. Security experts often take a few weeks to manually determine the CVSS base vector of a new vulnerability report. Consequently, the CVSS base vector is usually unknown for a period after the report is released, and thus delaying vulnerability countermeasures. Therefore, several methods for predicting CVSS base vector have been proposed. This paper compares the performance among methods that use BERT, multinomial logistic regression, or linear regression for automatically predicting CVSS base vector. The comparison results suggested that both BERT and MLR perform better than LR, with distinct advantages. BERT excels in understanding context, making it suitable for predicting general CVSS base vector, while MLR is effective for targeting specific attributes or severity levels. Consequently, these methods hold promise in aiding security engineers to promptly address vulnerabilities.

The UML (Unified Modeling Language) state machine diagram notation is challenging for learners to understand because of its complexity. Therefore, educators assign modeling assignments to learners to assess their understanding. If learners do not fully understand the notation, they may make errors in their diagrams. To improve learners’ understanding, educators provide the learners with explanations of what and why the diagrams unmet the requirements of the modeling assignments. However, the variety of content and layout in Learner-created diagrams can be challenging for educators to accurately and quickly identify the unmet requirements in each diagram. Therefore, this study proposes a method to semi-automatically identify and measure unmet requirements in Learner-created diagrams. The proposed method was applied to 38 state machine diagrams created by learners to evaluate its effectiveness. Consequently, the proposed method gave reasonable results for 37 out of 38 diagrams (approximately 97%).

In this study, we propose a method for applying a temporal relation identification model to functional requirements. We discuss the limited availability of data in the requirements engineering domain compared to other fields when used for supervised learning, and therefore employ a corpus from the news domain for training. The experimental results demonstrate that the types of temporal relations present in functional requirements are limited, indicating that focusing on learning with a narrowed set of labels is effective. Additionally, We incorporate Dependency Path (DP) into the temporal relation identification model and report, through comparative experiments, that leveraging DP is effective, but minor modifications to DP do not lead to significant improvements in accuracy. By demonstrating specific application methods of temporal relation identification in requirements engineering, we anticipate contributing to the analysis of functional requirements in software development.

In software development, ambiguities in requirements described in natural language (NL) prevent the application of formal approaches, posing a difficulty that has heretofore been avoided in two main ways: discovery based on formal specifications generated from NL requirements, and the creation of non-ambiguous NL requirements. In the former, NL is more expressive and does not rely on the user‘s expertise, but instead makes the automatic generation of formal specifications difficult. The latter facilitates the automatic generation of formal specifications and has the advantage of reduced syntactic complexity, but in exchange for reduced expressiveness of NL. In this paper, we take an approach that allows users to describe highly expressive NL requirements and reduces syntactic complexity to support the automatic generation of formal specifications from NL requirements. We also propose an information extraction method using syntactic patterns of low syntactic complexity. Applying our method to practical requirement sentences reveals that it is effective in reducing the complexity of information extraction rules. We expect that our method can support the automatic generation of formal specifications from NL requirements without compromising the expressive power of the language.

Model checking with a time aspect is often used in verification on hardware and embedded systems. Timed automata are often used for such models. UPPAAL is a world-wide famous model checking tool for timed automata; however, UPPAAL is a Computational Tree Logic (CTL)-based model checking tool and cannot use Linear Temporal Logic (LTL) properties. Bounded model checking uses LTL (Linear Time Logic) for a checking formula. Bounded model checking specifies a boundary k and obtains counterexamples by searching from the initial state of a system to states reachable by k-steps. There are several studies on bounded model checking. Sorea has proposed a concrete algorithm for a timed automaton. There are, however, no clear details on how to implement bounded model checking tools for timed automata, and study the performance. Another problem is that the timed automaton covered by the method does not support general variables except for clock variables. The objective of this study is to implement a bounded model checking tool using LTL for timed automata. We also improve Sorea's method so that it can handle extended timed automata that handle general variables. This paper also presents some LTL examples from texts on requirement specifications for embedded systems and the results of applying the tool to them.

A requirement specification for software is usually described in a natural language and thus may include sentences containing ambiguity and contradiction. Design errors due to ambiguous expressions and contradictions are often found later in the development process. These ambiguous sentences would force the developer to go back to the design process again. In order to prevent this kind of rework, a method of automatically converting a required specification written in Japanese to a state transition model is desired to help detect ambiguity and contradiction points of the specification. In previous studies, we have improved the extraction accuracy by refining the parsing rules. However, in order to parse a variety of sentences, it is necessary to set up new rules or refine the rules. In this paper, we propose a method of using a dependency analyzer in syntactic parsing. Using dependency analyzers eliminates the need for both of rule setting and refinement. Thus, the disadvantage would be eliminated. In addition, the effectiveness of the proposed method is reported by extracting and showing the elements necessary to create a state transition diagram.

In recent years, information systems have become large-scale and complicated. The demand for research on the cause analysis of information systems that can fail and the construction of countermeasures has been increasing. Systems Theoretic Accident Model and Processes (STAMP) is an accident model based on systems theory. STAMP has the feature that it can analyze not only failures of system components and human errors but also hazards caused by unsafe interaction between components and between components and humans. An analysis method based on the STAMP model System-Theoretic Process Analysis (STPA) is a method for analyzing in advance the possibility of a system accident for the interaction between a controller and a controlled device. As a preliminary study, we have performed STAMP/STPA to ‘Fallen Barrier Trap at Railroad Crossing,” which is an example of STAMP/STPA analysis. We have analyzed with the time automaton model checker UPPAAL in cooperation with STAMP Workbench, a STAMP/STPA support tool. From the preliminary study, we consider that the analysis procedure can be automated in order to reduce the burden on analysts. In this paper, we propose a method for deriving hazard transition sequences as a STAMP/STPA support method. Specifically, the model definition is described in STAMP Workbench, the method of deriving files that can be used in UPPAAL from the definition statement is described, and in order to automate model checking, the SAT/SMT solver is used. The constraints for the clock variables in each component are automatically derived. This paper describes a method for deriving the shortest path as a counterexample that does not satisfy the safety constraint equation by using the calculation method of the concrete value the constraints of and the binary search method. The proposed method is applied manually as the evaluation experiment. We confirmed that an effective sequence corresponding to some hazard scenarios derived by the conventional procedure could be derived.

In recent years, information systems have become large and complicated, and demand for research on accident analysis of such a system and its countermeasure construction is increasing. As an accident model based on system theory, Systems Theoretic Accident Model and Processes (STAMP) has attracted many attention. In STAMP, it is not limited to malfunctions of system components and human errors, but also has feature of possibility to analyze errors of interaction among constituent elements and interaction between constituent elements and human beings. System Theoretical Process Analysis (STPA) is a method for analyzing in advance the possibility of system accident against the interaction between the controller and the controlee. More effective accident analysis can be expected by cooperation of STAMP/SPTA and model checking based on formal method. In this paper, we describe a result of STAMP analysis example of “Fallen Barrier Trap at Railroad Crossing” with automaton model checker UPPAAL. In addition, we consider an automatic detection approach between the STAMP/STPA tool STAMP Workbench and the model checker UPPAAL.

The recovery of traceability links to requirements from a functional model created through analysis/design is crucial to understand existing systems for reuse, improvement or maintenance. Functional and non-functional requirements generally are implicitly interpreted and non-systematically woven into a functional model by analysts/designers. Traditional traceability link recovery methods focusing on terminology or syntactic structure, however, have a recovery limit because such interpretation and weave are not paid enough attention. This paper presents a novel idea to decompose such a functional model into model components in order to accurately trace a components to requirements especially non-functional requirements. We call such the decomposition traceability link mining. A screen transition model is adopted as the functional model because of the focus on usability.

This paper presents SMart-Learning, which is a set of state machine simulators for developing thinking skills. SMart-Learning handles a variant state machine diagram notation based on UML. The learners of the diagram require various thinking skills such as requirements analysis, concept formation including abstraction for a domain, and modeling conforming to the semantics. Evaluation of their diagrams is crucial in such learning but should not place an unnecessary burden on the learners when they use tools supporting the evaluation. However, usability aspects other than effectiveness of such tools has not received much attention. SMart-Learning provides three simulators to improve learners' skills step by step. Through an evaluation in which five learners use SMart-Learning, the effectiveness, especially usability, is discussed.

IoT devices are software-rich and Java is sometimes chosen as the developing programming language. Although Java is highly productive in constructing large advanced programs, application or user-defined Java classes must be responsible for safety and security issues. In particular, two fundamental methods hashCode and equals play key roles in safety and security assurance. Some existing studies for ensuring the correctness of these two methods rely on static analysis, which are limited to loop-free programs only. This paper proposes a new solution to this important problem, based on equivalence checking of methods or functions. The proposed approach makes use of software analysis workbench (SAW), an open source tool. The approach is also useful in reducing the cost of regression testing when program refactoring is conducted.

In recent years, Model-driven development (MDD) based techniques have emerged, and thus translation techniques such as translation from Object Constraint Language (OCL) to Java Modeling Language (JML) have gained much attention. We have been studying not only translation techniques from OCL to JML but also from JML to OCL in order to support Round-trip Engineering (RTE). Two directions of translation among OCL and JML are performed independently without considering unified and iterative translations in our previous work. For an OCL statement and another OCL statement which is obtained from a JML statement which was translated from the original OCL, our previous framework preserves only the meaning of the two statements, however, the forms of the OCL statements may change. It prevents us from RTE-based development. This paper proposes a translation technique between OCL and JML maintaining OCL code by describing their original forms in the comment area of the target languages. Our implementation has been evaluated on two projects used in our previous work and also seven additional open source projects.

Software visualization has attracted lots of attention. The techniques fall into two categories: visualization of software component relationships and visualization of software metrics.We have already proposed a hybrid method based on both of the two categories. The proposed method visualizes coincidence between specification and implementation from two aspects: static checking and ordinal testing by test suites. Each of the verification is performed in a method or function basis (unit testing). In the method, each ratio of the coincidence is shown by pie charts which represent classes of the target software. Whole software is represented in a weighted digraph structure.In this paper, we propose Priority Layout to emphasize important classes, and implemented our method into a tool. We have evaluated time in finding bug at source code and test cases between using Priority Layout, ISOM Layout and uncomplicated tables instead of graphs. As a result, time in finding bug at source code and test cases by proposed graph are a half of it using table.

Some methods for deriving protocol specifications from given service specifications with time constraints have been proposed. However, existing methods cannot treat the class of service specifications with both parallel synchronization and data values. They also assume that all clocks in the distributed system are synchronized. We propose an algorithm to derive a correct protocol specification automatically from a given service specification described in an extended model of time Petri nets where the above restrictions are eliminated. Using our method, we will be free from considering the details of communication delays on the design of real-time distributed systems.

In general, the services of a distributed system are provided by some cooperative protocol entities. The protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events which are described in a service specification of the distributed system. It is desirable that a correct protocol entity specification for each node can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes a correct protocol entity specification automatically from a service specification in a Petri Net model with Registers called PNR model. In our model, parallel events and selective operations can be described naturally. The control flow of a service specification must be described as a free-choice net in order to simplify the derivation algorithm, however, many practical systems can be described in this class. In our approach, since each protocol entity specification is also described in our PNR model, we can easily understand what events can be executed in parallel at each protocol entity.

The authors propose a synthetic technique to derive a correct protocol specification from a given service specification modeled as a nondeterministic extended finite state machine (EFSM). Each EFSM has a finite state control and a finite number of registers. In the model, the next state and the next values of the registers are determined depending on not only the current state and input but also the current values of the registers. The registers correspond to the system resources and they are allocated to some of the protocol entities in a distributed system. The derived protocol entities' specifications satisfy the resource allocation specified by the designer. A procedure solving 0-1 integer linear programming problems is used to reduce the number of the messages exchanged among the protocol entities.>