This study evaluates OSS project survivability using the Kaplan-Meier Survival Function and polynomial regression models. The key factors identified include the number of contributors and project popularity, which significantly influence survivability. Traditional indicators like project age do not directly correlate with OSS survivability. Instead, community engagement and recognition are crucial, offering valuable guidelines for managing and selecting Survivable OSS projects.

System-Theoretic Process Analysis (STPA) is performing a potential hazard analysis in the interactions of components within a system. Among STPA's process, deriving loss scenarios by identifying causes of the hazard has become increasingly important due to the complexity of modern systems. In this study, we utilize reinforcement learning to derive state transition paths that lead to hazard as loss scenarios, and extract the frequency of risk frequencies to demonstrate the necessity of safety measures for the respective loss scenarios. It is anticipated that this efficient approach will aid in simulating the system design process and enhancing safety.

Collaboration among team members plays a crucial role in the success of software projects. GitHub has emerged as a prominent platform for collaborative software development. This study focuses on analyzing GitHub repositories to gain insights into project status and participant characteristics based on development activities such as commits and pull requests. Utilizing a discrete time Markov chain, this research models GitHub repositories and employs probabilistic temporal logic and model checking to shed light on the activity levels of both projects and participants. We expect that understanding these observed trends and patterns can assist project managers in strengthening teamwork and fostering productive collaboration.

BOGOR model checking framework is developed for Object-Oriented software verification. It represents system as BIR (Bandera Intermediate Language). To model checking BIR, the BOGOR represents state as a node and transition as edge. First, BOGOR generates node and edge. Second, Model checking is performed in graph structure. However, this approach is inefficient to verify large software system. In this paper, we present symbolic model checking techniques to verify efficient BIR model checking. Experimental results show that the proposed algorithm can check more efficiently.

Multi-threaded Java programming such as an internet server program is difficult, because it is hard to detect subtle errors within multi-threading. LTSA is a too/for modeling and analyzing for catching some kinds of thread bugs, but still there remains scalability problem to deal with bigger applications. In this paper, we introduce a SAT based verification tool for Labeled Transition System and we explain LTS semantics and their CNF encoding. To verify large model, we focus our attention on efficient encoding for given model. In our tool, the property to be checked is expressed by either LTS or LTL formula based on Fluent. In order to solve a problem, LTSs and property are represented with CNF formulae, the input format to SAT-solver.