A Formal Verification Framework using Traceability-based Selective Model Projection for Large-scale Software

이동아 건국대학교 대학원 2019 국내박사

정형 검증 기법중 하나인 모델체킹은 안전 필수 시스템의 기능 정확성(functional correctness)를 확인하기 위하여 널리 사용되는 기법이다. 모델 체킹을 다루는 연구는 비교적 작은 규모의 소프트웨어를 대상으로 한다. 운영체제와 같이 크고 복잡한 시스템 전체를 모델체킹으로 검증하는 것은 불가능에 가깝다. 일반적으로 모델체킹을 사용하여 규모가 큰 시스템을 검증하고자 할 때는 소프트웨어를 기능이나 모듈 단위로 나눠서 검증을 수행한다. 하지만 단순하게 나눠진 기능이나 모듈을 검증한 결과는 소프트웨어 전체를 실행했을 때 발생할 수 있는 기능적 결함을 찾아내기는 어렵다. 따라서 대규모 소프트웨어를 대상으로 모델체킹을 수행하고자 할 때, 대상을 목적에 맞게 나누는 방식이 가장 중요하다. 본 논문에서는 추적성을 기반으로 검증 목적에 관련되는 소프트웨어의 특정 부분을 체계적으로 찾아낼 수 있는 선택적 모델 투영(Traceability-based Selective Model Projection) 기법과, 그 기법을 활용하여 대규모 소프트웨어의 정형검증을 수행하기 위한 프레임워크를 제안한다. 프레임워크를 사용해 검증을 수행하기 위해서는 소프트웨어 개발산출물 간의 추적성을 확보하는 것이 선행되어야 한다. 확보된 추적성을 바탕으로 소프트웨어를 수평적 관점 및 수직적 관점으로 모델링 및 검증을 수행한다. 수평적 관점은 소프트웨어 전체를 대상으로 넓고 얕은 모델을 생성하기 위한 관점이며, 수직적 관점은 검증 목적에 초점을 맞춰 소프트웨어의 특정 부분을 상세하게 다루기 위한 관점이다. 제안하는 선택적 모델 투영 기법은 수평적 관점으로 생성한 소프트웨어의 모델을 검증 목적에 맞게 시뮬레이션하고, 시뮬레이션 과정에서 활성화되는 영역을 도출하여 모델의 특정 영역을 도출한다. 모델 투영을 통해 도출한 수평적 모델의 특정 부분은 추적성을 활용해 소스코드와의 관계를 분석한다. 도출된 소스코드로부터 수직적 모델을 생성하고 모델 투영 과정에서 사용된 검증 목적을 사용해 수직적 검증을 수행한다. 제안하는 프레임워크를 사용하여 항공용 실시간 운영체제인 Qplus-AIR를 대상으로 정형검증을 수행하였다. 검증을 위하여 Qplus-AIR가 준수하는 ARINC 653-1 표준으로부터 검증 속성을 도출하였으며, 수평적 관점으로 시스템의 모델을 생성하기 위하여 Statemate를 사용하였다. 투영된 수직적 관점의 모델을 검증하기 위하여 3가지 (SPIN, Times, CBMC) 모델체커를 사용하였다. 사례연구를 통해 제안하는 검증 프레임워크가 대규모 소프트웨어를 검증하기에 적합함을 확인하였다. 또한 밝혀낸 Qplus-AIR의 문제점과 이를 해결하기 위한 방법을 개발팀에 보고하여 개선할 수 있도록 하였다. Model checking, one of formal verification techniques, is widely accepted as a useful technique to demonstration of functional correctness for software in safety critical systems. Most studies in application of the model checking have handled a relatively small example which has small amount of state space. Large and complex software, such as operating systems, is hardly possible to be verified as a whole, because model checking has limitation about size and complexity of the model. Although it is possible to apply model checking to the software divided into small parts by a function or a module, the simple division is not enough to verify the functional correctness of them working together. Therefore, identifying all parts of software relevant to the verification purpose is important for the verification using model checking. This dissertation suggests a formal verification framework using selective model projection based on traceability to identify specific parts of software with respect to verification purposes. The framework starts with establishing traceability between products of a software development process. Two verification approaches, a horizontal verification and a vertical verification, conduct modeling and verifying the software. The former models and verifies the software in a wide and shallow point of view which covers a wide range of the software but does not include detail information. The latter, on the other hand, models and verifies the software in a narrow and deep point of view which focuses on a specific parts according to a verification purpose. The selective model projection is a technique to identify relevant parts in source code with respect to a verification purpose for the vertical verification. The projection identifies relevant parts through simulating the model for the horizontal verification with a simulation scenario about a verification purpose. Traceability analysis leads to find the parts in source code that corresponds to the projected parts in the model for the horizontal verification. The parts of source code are modeled and verified in the vertical verification. This dissertation shows that a case study about verification of Qplus-AIR, which is a real-time operating system for avionics, demonstrates feasibility of the proposed framework. Verification properties are derived from the standard specification, ARINC 653-1 which Qplus-AIR complies. Modeling and verification of Qplus-AIR for the horizontal verification uses Statemate, and it checks whether the Statemate model satisfies the properties using a model checker and a simulator. Three model checkers, SPIN, Times, CBMC, are selected to verify models for the vertical verification. The result of the case study demonstrated the feasibility of the framework, and the verification found some property violations which were delivered to the development team.

An API-call Constraint Checking Framework for Automotive Control Software : 차량전장용 제어 소프트웨어의 제약사항 위반 검출을 위한 검증 프레임워크

김동우 경북대학교 대학원 2017 국내석사

An automotive software is one of a safety-critical software since unsafe behavior of it may result severe property damage or human injuries. A standard for automotive software OSEK/VDX publish a set of API functions together with a set of API-call constraints that should be followed by application software running on the operating system and states that violating such constraints may leads undefined system state of operating system which can be a source of system failure. As a support for checking such constraints of automotive software, this work presents an API-call constraint checking framework for automotive control software. It consists of two constraint checkers. The one is capable of checking constraints which violation of it can be decide with the behavior of operating system by adapting formal models of the underlying automotive operating system. While the other does not consider the operating system for the better performance. With abundant study for API-call safety checking, this study is the first study considering OS in API-call safety checking. 차량전장용 소프트웨어는 작은 결함으로 인해 인명피해와 같은 치명적인 문제를 일으킬 수 있으므로 안전 중요 소프트웨어로 분류된다. 차량전장용 소프트웨어 관련 표준인 OSEK/VDX에서는 차량전장용 소프트웨어의 API와 각 API의 사용상의 규칙을 정의하였으며, 각 사용상의 규칙이 위반되었을 때에는 운영체제를 비 정상적인 상태로 이끌 수 있다고 하였다. 본 연구에서는 차량전장용 소프트웨어의 API 호출 상의 제약사항을 검증하기 위한 검증 프레임워크를 소개한다. 이 검증 프레임워크는 검증 목적에 따라 운영체제의 행위와 연관된 제약사항을 검증할 수 있는 검증기와 운영체제의 행위와 관련이 없는 제약사항만을 빠르게 검증할 수 있는 검증기로 구성이 되어있다. 전자는 검증과정에서 운영체제 모델을 고려하여 운영체제의 행위와 연관된 제약사항을 포함한 모든 제약사항에 오탐 및 미탐없는 철저한 검증을 수행하는 것을 목표로 하며, 후자는 운영체제의 행위를 고려하지 않아도 되는 제약사항만을 검증함으로써 낮은 검증 비용으로 빠르게 검증하는 것을 목표로 한다. API 호출 안전성과 관련된 연구는 많이 진행되어 왔지만, 본 연구처럼 운영체제 모델을 고려하여 운영체제의 행위와 연관된 제약사항을 검증한 연구는 없었다.

자동화된 팩트체크 과정에서 딥러닝을 이용한 주장(claim) 판별 기법 연구

박성민 서울대학교 대학원 2022 국내석사

본 연구는 팩트체크 과정 중, 검증할 대상이 되는 주장을 판별하는 과정을 자동화해보고자 하였다. 이를 위해 팩트체크 검증대상 분류용 데이터셋을 직접 제작하였으며, 이를 기반으로 해당 데이터셋을 딥러닝 언어모델에 학습시켜 실질적으로 검증대상을 판별할 수 있는 분류 모델을 제작한 후 평가하였다. 본 연구에서 제작한 팩트체크 검증대상 분류용 데이터셋은 총 118,119개의 문장으로 이루어져 있으며 과거 한국 정치인의 발화 데이터(홈페이지, SNS, 국회회의록 등을 포함)를 기반으로 제작되었다. 각 문장은 팩트체크 대상이 되는 주장을 판별하기 위한 두 가지 기준인 '검증가능성'과 '검증중요성' 두 개의 이진 라벨을 지니고 있다. 사실적 정보에 대한 주장(factual claim)을 검증가능성이 참인 문장으로 분류하였으며, 이 중 실제 팩트체크의 대상이 되는 내용의 주장을 검증중요성이 참인 문장으로 보았다. 해당 데이터셋과 텍스트 분류 기법을 활용하여, 한국어 팩트체크에서 검증대상이 되는 주장을 판별할 수 있는 분류 모델을 제작하였다. 해당 분류 모델은 한국어 코퍼스를 사전학습한 딥러닝 언어모델인 KoBERT를 전이학습하는 방식으로 제작되었다. 검증가능성과 검증중요성 두 가지 라벨에 대해 각각 이진 분류 모델을 제작하였으며, 그 성능을 정확도, 정밀도, 재현율, F1-점수를 통해 평가하였다. 검증가능성 기준 분류 모델은 모든 지표에서 높은 성능을 보이는 모델을 제작할 수 있었으며 검증중요성 기준 분류 모델 또한 상당한 성능을 지니는 모델을 제작할 수 있었으나 정밀도 부분에서 약간의 한계를 보였다. 본 연구는 한국어 팩트체크 주장 판별을 위한 유의미한 크기의 데이터셋을 최초로 구축하였다. 해당 데이터셋은 이후 팩트체크 자동화 모델뿐만 아니라 한국어 자연어 처리를 위한 데이터셋으로도 활용될 수 있다. 또한, 직접 제작한 분류 모델이 상당히 높은 정확도로 작동하는 것을 확인하였다. 이는 추후 팩트체크 자동화 과정에서 해당 기법이 검증할 대상을 분류해내는 데 실질적으로 활용될 수 있음을 의미한다. This study attempted to automate the process of detecting check-worthy claims during the fact-checking process. Specifiaclly, we constructed a dataset to classify check-worthy claims, and based on this, we built a classification model using pre-trained deep learning language model. Our dataset consists of a total of 118,119 sentences and was produced based on past Korean politicians' utterance data (including websites, SNS, and minutes of the National Assembly). Each sentence has two binary labels: "Verification Possibility" and "Verification Importance," which are two criteria for check-worthiness. Factual claim was classified as a sentence with true verification possibility, of which the claim subject to actual fact check was viewed as a sentence with true verification importance. Using our dataset and text classification technique, we trained a classification model to detect check-worthy claims for Korean fact check. The final model was built by fine-tuning KoBERT, a deep learning language model which was pre-trained with the Korean corpus. Binary classification model was produced for each of the two labels of verification possibility and verification importance, and their performance was evaluated through accuracy, precision, recall, and F1-score. The verification possibility classification model showed high performance in all indicators, and the verification importance classification model also showed high performance in most indicators but the precision was relatively low. This study first constructed a dataset of significant size to detect the Korean chech-worthy claims. The dataset may then be used as a data set for Korean natural language processing as well as a automating fact-check. In addition, our check-worthy classification model performed considerably high accuracy. This means that in the process of automating fact-check, the technique can be practically used to detect check-worthy claims.

Bayesian Model Checking in Cognitive Diagnostic Models

Wang, Nan ProQuest Dissertations & Theses The Florida State 2019 해외박사(DDOD)

Checking that models adequately present data is an essential component of applied statisticalinference. Psychometricans increasingly use complex models to analyze test takers responses. The appeal of using complex cognitive diagnostic models (CDMs) is undeniable, as psychometricians can fit and build models that represent complex cognitive processes in the test while simultaneously controlling observation errors. With a trend toward diagnosing fine-grained skills that are responsible for test performance, both new methods and extensions of existing methods of assessing person fit in CDMs are required.Posterior predictive method (PP) is the most commonly used method in evaluating the effectiveness of person fit statistics in detecting aberrant response patterns in CDMs. It has been shown to be effective in detecting aberrant responses in IRT models but it is seldom implemented in cognitive diagnostic model. Additionally, two less known Bayesian model checking methods, prior predictive posterior simulation method (PPPS), pivotal discrepancy measure (PDM) will also be used to investigate the effectiveness of chosen person fit statistics. Three person fit statistics, log-likelihood statistic (l_z), un-weighted between-set index (UB) and response conformity index (RCI) are chosen in this study.In this study, I investigated the effectiveness of different Bayesian model checking methods in detecting aberrant response patterns with chosen discrepancy measures. The results from this study might help researchers answer the following two questions: (1) which discrepancy measure is more effective in detecting the aberrant response patterns under different model checking methods? (2) how well do the chosen discrepancy measures detect outlying response pattern? A simulate study was conducted to answer the above two questions. In terms of the data generation, it consists of two parts. One is for aberrant response pattern and the other is for normal response pattern. The normal response pattern is simulated from the DINA model with designated attribute parameters and each of four different aberrant response patterns was simulated by using binomial distribution with different assigned probabilities. The data was simulated and analyzed in R programming language and with Rjags package. Several interesting results can be drawn from my study: (1) increasing the test length did not improve the detection rates for each kind of aberrant response pattern. (2) Q-matrix complexity did not decrease the detection rate too much. (3) Generally speaking, loglikelihood statistic is the best measure in detecting each of different response pattern, especially for the cheating responses. (4) there isn’t too much performance difference of discrepancy measures under the PP and PPPS method. (5) Although the discrepancy measure RCI was developed in the context of cognitive diagnostic model (CDM), it had a poor performance in detecting each of the different aberrant responses.

소프트웨어 정의 제어기를 위한 자동차 안전보증 프레임워크 : 안전공학 전략과 확률적 안전 무결성 검증

정대희 경기대학교 대학원 2026 국내박사

SDVs(Software-defined Vehicles) represent one of the most advanced research and development technologies in the automotive industry, wherein vehicle control is determined and executed primarily through software. As SDVs continue to evolve, users are able to experience new values that transcend the traditional notion of automobiles as mere means of transportation, by integrating ICT(Information and Communications Technology) into vehicles through paradigms such as V2X(Vehicle-to-Everything). However, the emergence and development of SDVs have also introduced new challenges in the domain of safety assurance. Since software constitutes the foundation of control in SDVs, the overall system functions are realized through the extensive interactions of numerous controllers. Traditional reliability-based safety engineering techniques, which analyze components rather than interactions, are increasingly inadequate to guarantee the safety of such complex systems. In response, international standards governing automotive safety have also evolved. Beyond functional safety, as defined in ISO 26262, developers are now required to demonstrate SOTIF(Safety of the Intended Functionality) under ISO 21448. Thus, addressing the transformation of safety assurance in SDVs necessitates research that can both overcome the limitations of traditional safety engineering methods and achieve compliance with these dual standards. This dissertation proposes a safety assurance framework for SDVs, aimed at preventing accidents and ensuring system safety in safety-critical automotive applications through a stepwise process that supports the development of both functional safety and SOTIF, spanning from system analysis to safety verification. The proposed framework restructures system-theoretic hazard analysis and hierarchical reliability-based safety analysis, grounded in a CSD(Control Structure Diagram) modeled from the perspectives of Function, Behavior, and Structure. By adopting an MBSE(Model-based Safety Engineering) approach, the framework supports safety assurance that reflects the interaction-driven characteristics of SDVs. Furthermore, to enhance the accuracy and credibility of safety assurance results, this dissertation introduces a methodology that builds upon the results of hierarchical safety analysis to perform probabilistic safety integrity verification. System failure states and transitions identified in the safety analysis are formally synthesized into a Markov model, which is subsequently evaluated through probabilistic model checking to verify compliance with the ASIL(Automotive Safety Integrity Level). This approach mitigates potential systematic failures arising from variability in analyst judgment or methodology and enables safety analysis that accounts for uncertainties in empirical data, such as failure rates affected by thermal or aging phenomena. The proposed framework has been applied to the EPS(Electric Power Steering) controller under development at H Corporation to evaluate its validity. The results demonstrate that the framework systematically identifies potential hazards, derives safety requirements that maintain the system in a safe state, and confirms that these requirements are successfully implemented in the design. Furthermore, the quantitative verification shows that the safety integrity goals anticipated during the analysis phase are met, thereby substantiating the assurance of SDV safety. The contributions of this dissertation to the safety assurance of software-defined controllers are threefold: (1) preventing the omission of potential accident hazards that may arise due to the unique characteristics of SDVs, (2) establishing a safety assurance framework tailored to the automotive domain on the basis of MBSE, and (3) improving the consistency and reliability of safety analysis results through formal synthesis and probabilistic model checking. SDV(Software-defined Vehicle)는 자동차 산업에서 다루어지고 있는 최신의 연구개발 기술로, 소프트웨어에 의하여 자동차 시스템의 제어를 결정 및 처리한다. SDV가 발전해 나아감에 따라 사용자는 이동수단 이라고 하는 한계를 넘어, 자동차에 ICT(Information and Communications Technology) 기술을 융합한 V2X(Vehicle to Everything)의 새로운 가치들을 경험할 수 있게 되었다. 한편 SDV의 등장과 발전은, 자동차의 안전보증(Safety Assurance) 연구 분야에도 새로운 도전과제를 가지고 오게 되었다. 소프트웨어를 제어의 근간으로 하는 SDV는, 자동차를 구성하는 다양한 제어기의 수많은 상호작용을 중심으로 기능을 제공한다. 그러나 기존의 신뢰성 기반 안전공학 기술은 상호작용이 아닌 구성요소를 대상으로 분석을 수행하기 때문에, 시스템의 안전을 보증함에 있어 한계점이 생기기 시작하였다. 자동차의 안전보증을 위해 국제적으로 약속된 규격에도 변화가 발생하였다. SDV에 대한 기능안전(Functional Safety) 뿐만 아니라, 운용안전(Safety of the Intended Functionality)까지 달성하여 안전이 보증되었음을 증빙하도록 요구하게 된 것이다. 이처럼 SDV를 위한 안전보증 분야의 변화를 대응하기 위해서는, 기존의 안전공학 기술이 가지는 한계점을 극복하면서도 두 가지 안전 규격을 달성할 수 있는 방안에 대한 연구가 필요하다. 본 논문에서는 안전 필수(Safety-critical) 시스템의 하나인 SDV의 사고를 예방하고 안전성을 보증하기 위하여, 모델을 중심으로 분석부터 검증까지 단계적으로 기능안전과 운용안전의 개발을 돕는, 자동차 안전보증 프레임워크를 제안한다. 제안하는 프레임워크는 시스템 이론, 특히 FBS(Function, Behavior, Structure) 관점으로 설계된 CSD(Control Structure Diagram)를 기반으로, 시스템 이론적 위험원 분석(System Theoretic Hazard Analysis)과 신뢰성 기반 계층적 안전 분석(Hierarchical Reliability Safety Analysis)을 수행할 수 있도록 재구성하여, SDV의 상호작용을 중심으로 기능안전과 운용안전을 보증할 수 있는 MBSE(Model-based Safety Engineering) 체계를 구성한다. 또한 본 논문에서는 안전보증 결과의 정확성을 향상시키기 위해, 확률적 안전 무결성 검증으로 신뢰성 기반 계층적 안전 분석을 수행한다. 안전 분석에서 파악한 시스템의 고장 상태 및 천이 관계를 정형 합성(Formal Synthesis)을 통해 마르코프 모델(Markov Model)로 변환하고, 확률적 모델 검증(Probabilistic Model Checking)으로 SDV의 ASIL(Automotive Safety Integrity Level)을 검증한다. 이를 통해 안전보증 결과의 정확성에 영향을 미칠 수 있는 시스템적 고장(Systematic Failure)을 최소화 하고, 분석 데이터의 불확실성까지 고려하는 안전 분석의 수행을 돕는다. 본 논문에서 제안하는 방법은, H사에서 개발하는 EPS(Electric Power Steering) 제어기에 적용하여 유효성을 확인하였다. 그 결과 프레임워크에 따라 시스템이 가질 수 있는 위험원(Hazard)을 체계적으로 식별하고, 시스템이 항상 안전 상태에 머물 수 있도록 위험원을 제어하는 안전 요구사항이 도출되었음을 확인할 수 있었다. 그리고 나아가 도출된 안전 요구사항이 실제 시스템에 설계되어, 분석 단계에서 예측하였던 안전 무결성이 요구하고 있는 목표 값만큼 SDV의 안전보증이 달성되었음을 정량적으로 확인할 수 있었다. 본 연구가 소프트웨어 정의 제어기의 안전보증에 기여하는 부분은 세 가지이다. 첫째, SDV의 특성으로 인해 분석 과정에서 누락될 수 있는 사고의 위험원을 방지한다. 둘째, MBSE 체계를 기반으로 SDV에 적합한 자동차 분야의 안전보증 체계를 수립한다. 셋째, 정형 합성 및 확률적 모델 검증을 통해 일관적인 안전 분석 결과를 도출하고 나아가 안전보증 결과의 신뢰성을 향상시킨다.

A New Calibration Metric ? Probability Residual (PR) and Its Validation Practice for Rotor Dynamics Model of a Journal Bearing Rotor System

최환오 서울대학교 대학원 2016 국내석사

In constructing the computational model of engineered systems such as a journal bearing rotor systems, statistical model calibration method is often used since the statistical model emulates the actual behavior of the engineered systems with uncertainties. A calibration metric, which quantifies the degree of agreement or disagreement between computational and experimental results, is one of the key components in the statistical model calibration. However, some existing calibration metrics such as log-likelihood and Kullback-Leibler divergence (KLD) have limitations in constructing an accurate computational model. To overcome this problems, this study proposes a new calibration metric, probability residual (PR). The PR metric is defined as the sum of the product of scale factor and square of residuals. The scale factor scales the PDF in specific range, which enables to improve the calibration efficiency. The square of residuals makes the PR a convex form, which guarantees existence of global optimum. So as to evaluate the performance of the PR metric, this study uses mathematical models and employs statistical models of the journal bearing rotor system appropriate to normal and rubbing state. As a result, the PR metric performed better than other metrics including log-likelihood and KLD in terms of the calibration accuracy and efficiency, and the calibrated journal bearing rotor model with PR was proved in valid by the hypothesis testing. In summary, the proposed PR metric is promising to be applied in building an accurate computational model.

A Model Checking Approach for Conflict Detection and Service Selection in Service Oriented Environment

김연석 연세대학교 대학원 2011 국내박사

Recently, with the wide spread of Web services in various fields, there is a growing interest in composite Web services that provide sophisticated functions by composing Web services. However, due to the complexity, time consumption and high cost for composing services, automatic composition is needed. In addition to these problems, composite Web services, which are automatically constructed, may contain various and unintended errors and thus, a safety verification on these services is necessary. This thesis proposes an efficient method for detecting conflicts which may occur at the design-time of service composition, and identifying the causes. Also, in order to increase the re-usability of composite Web services, we propose an efficient service selection method based on model checking. The proposed method divides and refines the correctness claims into three types: precondition, policy and assumption. The precondition, policy, and assumption of a service are defined as the constraint conditions that should be met prior to the service execution, during execution, and at all times, respectively. Meanwhile, the proposed method models composite Web services and the correctness claims by using OWL-S and SWRL, and automatically converts them into system models and temporal logics, respectively. After that, we detect conflicts through model checking. Experimental results on real world composite services show that the proposed method detects conflicts in composite Web services effectively. Additionally, this thesis proposes an efficient service selection method that verifies the state conditions of services based on model checking. The proposed method not only can select a service which fully satisfies the requirements, but it can also select a service that satisfies the requirements partially. Also, we calculate the suitability of a service and sorts the services depending on their values. To evaluate the performance of the proposed method, we experimented with 150 services and 10 requirements. The result shows that the proposed method has performed better compared with previous works. This thesis demonstrates the usefulness of a formal verification technique, model checking, in conflict detection and service selection of a composite Web service. Particularly, the proposed method not only considers the conflicts that can be detected at the design-time of service composition, but it also is very helpful in identifying the conflicts that may occur during service execution. In addition, since the proposed method describes services and correctness claims with a familiar language in the Web services field, even the service developers who are unaware of a system model and temporal logic can easily verify the services. Meanwhile, by applying model checking to the service selection field, an efficient service selection is possible.

Applying AI Technology to Recognize 3D Objects and Visible Properties for Automatically Checking Modular BIM Objects

HONGWEI SUN 경희대학교 대학원 2022 국내박사

With the increasing popularity of modular buildings, many manufacturers have supplied BIM objects for their products allowing use by designers, such as modular bathroom BIM object and modular kitchen BIM object, these products are different from general components and need to meet the requirements of certain use functions, building regulations, and corresponding transportation conditions, etc. Even if designers can get the corresponding modular BIM objects, they cannot use it directly, and the quality of the BIM model needs to be further verified. Currently, there is a lack of automated verification systems for modular BIM objects. With the emergence of automated code checking technology, the compliance of BIM data can be checked, therefore the author proposes to make a separate verification system for modular BIM objects based on automated code checking technology. From current technology, it is possible to create modular BIM object guideline and develop a corresponding modular BIM object verification system. However, users need to input BIM model information accurately to make sure the checking results correct. As this process involves human inputs, it is difficult to ensure that each input is accurate. In the case of errors or missing inputs, the checking results will be erroneous. Although automated checking systems can be developed accurately, it is difficult to apply these systems practically. Since the automated code checking system primarily depends on the identification of BIM objects and properties. The existing information inputting method principally depends on manual inputs, which require significant efforts from users. Therefore, in this study the author proposes the application of AI technology to recognize BIM objects and visible properties, in order to improve the operability of automated code compliance checking. The two necessary elements - object names and properties - could be automatically extracted to a certain extent, following the application of the proposed method to the automated code checking process. The error rate of the input could also be reduced, thus making the application of the code checking system more practically feasible. The proposed recognition method for BIM objects and visible properties is expected to be widely used in BIM-based building e-submission systems and BIM-based forward designs. Meanwhile, an AI-based automated modular building BIM object verification system is also proposed to promote the supply of modular buildings in this study. This can become a platform that connects designers and suppliers when applied to the modular building product certification site of a government or relevant institution. The verified BIM modular object can serve as a national real-time update standard BIM library. Designers can use standard modular BIM objects to improve design productivity. Since the modular BIM object verification system uses the same ruleset as the national BIM-based building e-submission system, if the designers use the verified modular BIM object for designing, it can also facilitate the building e-submission process.

Steel Box Girder교의 해석 및 설계업무 효율화를 위한 객체지향 데이터모델 방법론 연구

박재우 연세대학교 대학원 2002 국내석사

In this study, a data model which can be applied to design check system through object-oriented modeling technique was developed on the focus of Steel Box Birder Bridge. The data model ensures effective reuse of analysis information data generated repeatedly during design and analysis procedure. In the developing procedure, the design check process was analysed step by step by using IDEF0(Integration DEFinition for function modeling) technique and a process model was made by extracting required input and output data from each process and then subsequently, the data model was constructed by using UML(Unified Modeling Language). For efficient management of structural data of the bridges, the data model was decomposed into modeling part, structural analysis part, design check part and global, local and component elements parts. In the process of developing the data model, bridge design specification, bridge design standards and bridge design manuals which give guidelines to design check work was referred and used to express the data model. /In order to verify the compatibility, effectiveness and applicability of the proposed model, both conventional structural data modeling method and newly proposed data modeling method were applied to the design process of real structure and then comparison and analysis for the methods were performed. The design data model proposed in this study is based on object-oriented modeling methodology concept, which makes it easy to add, modify and maintain information. Also, it can be used to manage various information needed in design check process during the life-cycle of the bridges and efficiently applied to operating design check system and data together./ 본 연구는 Steel Box Girder교를 대상으로 하여 해석 및 설계단계에서 반복적으로 발생하는 해석정보 데이터를 효율적으로 재활용하고 다량의 정보를 객체 모델링 방법론을 적용하여 해석 및 설계검토 시스템에 응용할 수 있는 데이터모델을 개발하였다. 이를 위하여 IDEF0(Integration DEFinition for function modeling) 방법론에 따라 Steel Box Girder교의 해석 및 설계 단계별로 프로세스를 분석하고 각 프로세스별로 필요한 입출력정보들을 추출하여 프로세스모델을 구성하였으며, 이를 토대로 객체 모델링 언어인 UML(Unified Modeling Language)을 사용하여 데이터모델을 작성하였다. 이 때, 교량 구조물의 정보를 효율적으로 관리하기 위한 방안으로 구조모델링, 구조해석, 구조설계검토의 작업관점 및 전체, 부분, 부재요소의 계층구조로 분류하여 모델을 구성하였다. 데이터모델 개발 시 기준으로서는 교량 설계업무의 기준이 되고 있는 도로교설계기준, 도로설계편람 등을 참고로 하였으며 이를 데이터모델에 표현하였다. /개발된 모델의 적합성을 검증하기 위하여 기존의 실무에서 사용했던 전통적인 구조 모델링 방법과 본 연구에서 제안된 객체지향 데이터 모델링 방법을 실제 사례구조물에 대하여 각각 적용하고 이를 비교 분석하므로써 그 효용성 및 적용 가능성을 검증하였다. 본 연구에서 제안한 데이터모델은 구조해석 및 설계작업 시 정보추가, 수정 및 재활용이 용이한 객체 모델링 방법론을 적용하여 구성하였으며 추후 해석 및 설계에 이용되는 다양한 정보들을 교량의 생애주기동안 효율적으로 관리하는데 이용될 수 있고 해석 및 설계검토 시스템과 데이터를 연동시키는데 효과적으로 적용될 수 있다. /

설계단계에서의 효과적 VE적용을 위한 기능정의 프로세스 모델

민경석 연세대학교 대학원 2001 국내박사

본 논문은 효과적 설계단계에서의 Value Engineering(이하 설계VE)활동을 위하여 기능분석의 시작이라 할 수 있는 기능정의의 구성요소를 분석 및 정리하여, 기능정의의 체계적인 활동방법을 유도하는 기능정의 분석 프로세스에 관하여 연구하였다. 본 연구에서 제시한 기능정의 명사부 분석 프로세스를 통하여 다음과 같은 사항을 결론적으로 정리할 수 있다. 1. 기능정의 분석 프로세스의 구성 기능정의에 대한 효율적인 활동을 위하여 본 프로세스는 우선적으로 검토수준의 결정을 요구한다. 여기서 설정된 수준으로 중요도 및 만족도 개념을 이용하여 Value Engineering(이하 VE)활동의 주 검토대상을 선정하고, 이를 다시 기능적으로 표현하는 명사부를 분석기준과 활동상황에 따라 대표명사로 재분류, 체계화하여 효과적이고 신뢰성 있는 기능정의를 마련한다. 또한 실질적인 VE활동에 적용하기 위하여 공동주택을 대상으로 한 활용방법에 대하여 제시한다. 2. 기능정의 분석 프로세스의 효과. 본 프로세스는 주관적으로 시행되어온 기능분석 작업을 체계적이고 분석적인 방법으로 유도하고, 기능분석 활동시 오류발생 부분을 쉽게 발견할 수 있으며, 프로젝트의 진행에 따른 검토수준을 통일하여 체계적인 기능분석 활동을 기대할 수 있다. 또한 프로젝트의 진행 정도에 따라 검토수준을 다르게 설정, 분석함으로 폭 넓은 활용이 가능하며, 중요도 및 만족도에 의한 주 검토대상의 선정으로 효율적인 VE활동을 기대할 수 있다. 여기에 대표명사의 선정방법은 체계적 활동뿐만 아니라 기능정리를 위한 Function Analysis System Technique Diagram(이하 FAST Diagram)의 용이하고 효과적인 작성을 유도할 수 있다. 3. 프로세스 활용시 주의사항. 본 프로세스는 과정상 설정한 기준을 중심으로 기능정의의 명사부를 분석하였음으로, 분석기준의 특성 이외의 분야에서의 기능파악이 약화될 수 있으므로, 프로젝트의 성격과 활동목표를 명확하게 파악하여 최적의 분석기준을 설정, 효과적으로 활용할 수 있는 방안을 마련해야 한다. 또한 본 프로세스에서 주관적 평가 부분은 프로젝트에 대한 많은 경험과 축적된 자료를 통해 신뢰성을 높여야 하고, 검토레벨 선정, 주 검토대상을 위한 평가 및 분석을 위한 기준 설정시 프로젝트의 성격과 분석목적의 충분한 이해를 위해 VE팀원들의 논의가 있어야 한다. 4. 프로세스를 위한 향후 연구방향. 본 프로세스는 현실적으로 설계VE가 아직까지 초기단계로 대상프로젝트에 대하여 분석활동이 충분하지 못했음으로, 본 프로세스가 향후 많은 프로젝트를 대상으로 설계VE 활동이 이루어질 경우 발생하는 오류 또한 체계적으로 분석하여 확고한 기능정의 분석 프로세스를 정립해야 하겠다. 여기에 세분화, 체계화된 검토레벨의 설정연구, 설계VE 주 검토대상의 선정을 위한 평가방법에 대한 연구, 대표명사의 선정방법에 관한 체계적인 연구, 각 프로젝트 별로 다양한 분석기준 설정에 관한 연구 등이 실시되어야 한다. 또한 기능분석을 위한 활용명사의 체계적인 정리 및 Feed Back작업, 각 프로젝트 별로 다양한 분석기준 설정 및 설계VE의 각 단계에 대하여 활용 가능한 모델과 프로세스의 다양한 연구가 필요하다. This thesis is an analysis and summary of the structural elements of the function definition, the foundation of the function analysis for the effective application of VE(Value Engineering) and a study of the function definition process model. The function definition analysis of this paper can be summarized as follows using function. 1. The Structure of the Function Definition Process Model. In order for the effective action of the function definition, the process requires a check level. The quality established by this process uses the concept of importance degree and satisfaction degree to establish the main check object of the VE activity. Then, depending on the analysis and activity of the noun parts that display these values as functions, they are reclassified as main nouns and organized into an effective and trustworthy function definition. One application method, a community dwelling house, is presented for the actual application of the VE. 2. The Effect of the Function Analysis Process. This process has been used as a supervisory processor, inducing structure and an analytical method, allowing for the easy detection of errors during function analysis and structural function analysis activity can be expected from the standardization of the inspection levels. In addition, broader application is possible through the differing check levels and analysis throughout the different phases of the project and more effective VE application can be expected from the selection of the main check object based on the importance and satisfaction degrees. Not only is the selection of the main check object good for structural application, it also induces effective turn out of the FAST Diagram for function arrangement. 3. Caution When Using the Process This process is useful for the analysis of noun parts based on the established process. Therefore, functional analysis in areas other than the particular analyzing standard can be weak and the characteristics of the project and the goal of activity must be clearly identified for ideal establishment and effective application. In addition, the reliability of the subjective evaluation of the process must be raised through much researched data and discussion must be held with VE team members before setting the standard for the selection of check level and evaluation and analysis for a main check object and for a complete under standing of the analysis and characteristics of the project. 4. The Future Direction of Research for the Process Currently, the design VE activities is still in the beginning stages and the analytical activity of the process on the respective project is insufficient. Therefore, henceforth, a function analysis process must be established based on the analysis of the errors and structure of the design VE activities that result from the application of the process to many, diverse projects. As follows, a subdivided, organized inspection level research, an evaluation research for the establishment of the main check object, a systematic research for the selection method of the main noun and research for the establishment of analytical standards across various projects is needed. In addition, various studies are needed for systematic management of the practical noun and feedback work for function analysis, the establishment of various analytical standards for different projects and active models and processes for each step of the design VE.