동적 시스템 명세를 위한 시제논리언어와 그 검증

조승모,김형호,차성덕,배두환,Cho, Seung-Mo,Kim, Hyung-ho,Cha, Sung-Deok,Bae, Doo-Hwan 한국정보과학회 2002 정보과학회논문지 : 소프트웨어 및 응용 Vol.29 No.7

Many modern complex systems, including most object-oriented systems, have dynamic characteristics that their components are dynamical]y configured during run-time. However, few analysis techniques are available that consider the dynamic nature of systems explicitly. We propose a specification and analysis method for these dynamic systems. We design a new temporal logic, called HDTL, to specify the properties of dynamically evolving systems, and tune up the tableau method for this logic. HDTL incorporates variables and quantifiers that enable the automatic analysis. Using HDTL and the analysis method, we can specify the correctness requirements of systems and check whether the system actually agree with the requirements or not. An experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique works well. 대부분의 객체지향 시스템을 비롯한, 복잡한 시스템들은 그 구성요소들이 시스템의 수행시간 중에 변하는 동적인 특성을 가지고 있다. 하지만 대부분의 기존 분석기법들은 이러한 측면을 무시하고 있다. 이 논문에서는 이러한 동적 시스템을 명세하고 분석하기 위한 기법을 제안하고자 한다. 이를 위해, 동적 시스템의 명세를 기술하기 위한 새로운 시제논리인 HDTL을 제안하고, 기존의 시제논리를 위한 분석기법을 수정하여 새로운 tableau 기법을 제안하였다. HDTL은 변수와 한정자를 사용하여 동적 시스템의 자동적 분석을 가능하게 하였다. 이 기법을 사용하여 우리는 시스템의 요구사항 명세를 기술하고, 시스템의 수행이 그 명세를 만족하는지를 살펴 볼 수 있다 실험을 통해 HDTL과 분석기법의 적용성을 보였다

HDTL을 이용한 병렬 자바 프로그램의 모니터 링과 검사

조승모,김형호,차성덕,배두환,Cho, Seung-Mo,Kim, Hyung-Ho,Cha, Sung-Deok,Bae, Doo-Hwan 한국정보과학회 2002 정보과학회논문지 : 소프트웨어 및 응용 Vol.29 No.5

There have been many researches about monitoring and checking the implementations during run-time using formal requirement specification. They usually adopt temporal logics or their extensions to specify the requirements for the implementations. However, most of the systems fail to support the specification of requirements fir dynamic systems - systems whore components are created and removed during run-time. Unlike analysis or design models, most actual implementations are dynamic, so the notion of instances should be employed in the property specification language. In this paper, we show how we can monitor and check Java programs using our temporal logic for dynamic systems (HDTL). We suggest a framework in which the execution of Java programs are monitored and chocked against given HDTL requirements. 정형 명세를 이용하여 구현된 프로그램이 수행 중에 명세를 만족시키는지 모니터링하고 검사하는 기법에 대한 연구들이 기존에 많이 수행되어 왔다. 이들은 주로 요구사항 명세언어로 시제논리 혹은 그것의 확장을 사용하게 된다. 이때 대부분의 연구는 실제 구현된 시스템이 가지는 동적인 변화를 제대로 요구사항 명세에 기술하고, 검사할 수 있는 언어를 제공하지 못하고 있다. 본 연구에서는 동적 시스템의 특성 명세언어로 기존에 제안했던 HDTL을 사용하여 동적인 자바 프로그램의 수행을 모니터링하고 검사하는 프레임웍을 제안한다.

연구개발, 무형자산, 소유집중이 기업생존에 미치는 영향 : 상장 중소제조업체를 중심으로

조승모(Cho Seung Mo) 부경대학교 인문사회과학연구소 2016 인문사회과학연구 Vol.17 No.1

본 연구에서는 2011년 12월 현재 KOSPI 시장과 KOSDAQ 시장에 상장되어 있는 12월 결산 중소제조업체 541개를 대상으로 생존분석을 실시한 결과, 대주주로의 소유권 집중이 경영자의 대리인 문제를 규율하는 긍정적인 역할을 하는 동시에 경영자가 기술혁신의 성과인 무형자산을 활용하는 것을 제약하여 무형자산이 기업의 생존성을 향상시키는 효과를 떨어뜨리는 역할도 할 수 있음을 알 수 있었다. 뿐만 아니라, 무형자산이 기업의 생존성을 향상시키는 역할을 하는 동시에 경영자 대리인 문제의 수단으로 활용될 수 있음도 알 수 있었다. 그리고 연구개발 활동은 그 불확실성으로 인해 기업의 생존을 위협하는 요인임을 알 수 있었다. 이를 통해, 기술혁신은 직접 연구개발을 통해서 하는 것보다 기술구매나 M&A를 통해 우선적으로 추구하는 것이 바람직하며, 소유권이 분산되어 있는 기업일수록 기술혁신을 통해 더욱 생존성을 향상시킬 수 있다는 실무적인 함의 또한 얻을 수 있었다. In this study, we have analyzed corporate survivability of 541 Korean manufacturing SMEs with fiscal year ending at the end of December listed in either the KOSPI market or the KOSDAQ market as of December 2011. As a result, we have found out that ownership concentration can effectively mitigatethe managerial agency problem while it can hinder the management in utilizing intangible assets, the result of technological innovation, reducing intangible assets’ corporate-survival-enhancing effects. Moreover, we have also found out that intangible assets can enhance corporate survival while they can be abused as a means of managerial agency problem at the same time. Furthermore, we have additionally found out that R&D activities, due to their uncertainty, can threaten corporate survival. These findings imply that technological innovation should first be pursued through technology purchases or M&As rather than through R&D and that corporations with a relatively diversified ownership structure can more greatly enhance corporate survival through technological innovation.

LUSTRE 를 이용한 SCR 명세의 구현

조승모(Seung Mo Cho),차성덕(Sung Deok Cha) 한국정보과학회 1999 정보과학회논문지(B) Vol.26 No.2

SCR 방법론은 고 신뢰도를 요구하는 시스템 개발을 위해 사용되는 요구사항의 정형적 명세의 하나로, 오랜 역사와 많은 응용 사례를 가지고 있다. 이 방법론에 따라 사용자가 요구사항을 명세했을 때 그것을 어떻게 정확하게 구현할 수 있는지가 중요한 문제가 된다. 본 논문에서는 SCR로 작성된 명세를 그 의미를 보전하는 구현언어로 자동으로 변환시키는 방법을 제시한다. SCR 명세가 가지는 자료흐름 언어와의 유사성을 이용하기 위해, 구현언어로 동기적 자료흐름 언어인 LUSTRE를 선택했고, 그 변환 과정을 제시하였다. 제안한 방법의 유용성을 살피기 위해, SCR과 유사한 방법으로 작성된 월성 원자력 발전소의 제 2 정지 시스템의 일부분을 변환하는 실험을 수행, 그 결과를 비교하였다. 정형명세가 도입되어서 사용될 경우, 본 연구는 개발의 전체 소요시간을 줄여줄 수 있고 좀더 신뢰성있는 결과물을 내는데 도움을 줄 수 있다. Formal specification and verification of software requirements is now gaining popularity in the field of safety-critical embedded systems. SCR (Software Cost Reduction) is one of such formal methods that has been applied to several real-world projects. We propose a procedure that translates an SCR specification into an executable program written in the sequential implementation language, such as C. We exploit the similarity between basic semantic models of SCR and the synchronous data-flow langauge LUSTRE. An SCR specification can be translated into a LUSTRE program of same meaning, and then, existing LUSTRE compiler can produce a sequential code. The correctness of our method is explained based on the formal semantics of SCR. To demonstrate the practicality of the method, a small portion of the requirement specification of Wolsung shutdown system 2, which is specified in SCR-like method, is translated into LUSTRE. We compare the result with the original code, and give some evidence of the practicality. This method may reduce the development time and increase the reliability of the final product when applied to the formal specification.

한국기업의 기업지배구조 기제로서 해외부문의 역할

조승모 ( Seung Mo Cho ),이필상 ( Phil Sang Lee ) 한국금융공학회 2011 금융공학연구 Vol.10 No.1

본 논문에서는 기업지배구조 기제로서 해외부문의 역할에 대해 논의하였는데, 해외부문을 외국인소비자, 외국인주주, 외국인채권자의 세 부문으로 나누어 이들의 역할을 분석하였다. 2002년부터 2008년까지 KOSPI 시장 및 KOSDAQ 시장에 상장되어 있는 1,009개 제조업체를 분석한 결과, 외국인주주들은 경영자에 대한 활발한 감시활동을 통해 대리인문제를 경감시키는 것으로 나타난 반면, 외국인소비자와 외국인채권자들은 경영자에 협조하거나 경영자의 부정행위를 묵인하여 대리인문제를 악화시키는 것으로 나타났다. 이는, 외국인주주들은 선진적인 경영기법과 경영자감시기법을 토대로 경영자의 사적효용추구를 효과적으로 저지하는 데 반해, 외국인채권자와 외국인소비자들은 정보비대칭, 지리적 거리, 언어적, 문화적, 법률적 상이성 등으로 인해 그렇게 할 수없기 때문인 것으로 보인다. 이러한 결과는 확률효과 패널 회귀분석, 확률효과 AR(1)패널 회귀분석, 확률효과 도구변수 패널 회귀분석과 같은 여러 상이한 통계기법을 적용하여도 동일한 결과를 유지하는 바, 통계적으로 강건한 결과임을 확인할 수 있었다. In this paper, we discuss the role of the foreign sector as a corporate governance mechanism. We divide the foreign sector into three: foreign consumers, foreign shareholders, and foreign creditors. Analyzing 1,009 manufacturing companies remaining listed in the KOSPI and KOSDAQ markets of Korea from 2002 to 2008, we show that foreign shareholders play an active monitoring role on the management alleviating the agency problem while foreign consumers and foreign creditors tend to cooperate with managers or countenance managers` misconducts worsening the problem. Foreign shareholders seem to effectively deter managers` pursuit of private benefits through advanced monitoring and managerial skills. However, foreign creditors and foreign consumers do not due to information asymmetry, geographical distances, and linguistic, cultural, and legal differences. Such a result has been confirmed robust to different statistical techniques of the random effects panel regression analysis, the random effects AR(1) panel regression analysis, and the random effects instrumental variable panel regression analysis.

기업 생존분석을 통한 네오 러다이트 운동의 지속성에 대한 고찰: 우리나라 상장 ICT 제조업체를 중심으로

조승모 ( Seung Mo Cho ) 아시아문화학술원 2016 인문사회 21 Vol.7 No.1

본 연구에서는 우리나라 ICT 산업에 속한 제조업체들 중 KOSPI 시장과 KOSDAQ 시장에 상장된 기업들을 대상으로 생존분석을 실시하여, 생산과정의 자동화 정도, 고용규모, 종업원의 질적 수준이 기업의 생존에 미치는 영향을 분석하였다. 생산과정의 자동화 정도는 노동장비율로, 고용규모는 기말에 측정된 종업원수 합계로, 종업원의 질적 수준은 종업원 1인당 연간평균임금으로 각각 측정하였는데, 이들 세 변수는 모두 독립적으로 기업의 생존성을 향상시키는 것으로 나타났다. 따라서 생산과정의 자동화가 반드시 고용악화나 임금하락으로 이어지는 것은 아니며, 생산과정의 자동화를 통해 단순노동을 기계로 대체하면서 고급인력의 채용을 늘리는 것은 기업의 생존성을 향상시키는 정책이라 할 수 있다. 기업들이 이러한 정책을 고수하는 한 기업들은 오래도록 살아남아 계속 이러한 정책을 추진하게 될 것이므로, 네오 러다이트 운동은 그 목적을 이루기 힘들 것으로 보인다. 최소한 우리나라 ICT 제조업계에서는 말이다. This study has carried out a survival analysis on Korean ICT manufacturing corporations listed either in the KOSPI market or in the KOSDAQ market to investigate the impacts of production automation, firm employment size, and qualitative level of labor on firm survival. Using the labor equipment ratio, the total number of employees, and the average annual salary per employee as proxies for production automation, firm employment size, and qualitative level of labor respectively, we have found out that these three variables independently enhance firm survival. This implies that production automation does not necessarily worsen employment nor does it reduce wages and that it is a firm-survival-enhancing policy to replace low-skilled labor with production automation and additionally hire high-skilled labor. As long as firms stick to this policy, they will survive longer and as long as they survive, the policy will persist. Thus, neo-Luddism does not seem to have bright prospects at least in the Korean ICT manufacturing industry.

Levy과정 하에서 추세와 도약이 있는 경우 옵션가격결정모형: Gerber-Shiu 모형을 중심으로

조승모 ( Seung Mo Cho ),이필상 ( Phil Sang Lee ) 한국재무관리학회 2007 財務管理硏究 Vol.24 No.4

논문 : 기업지배구조와 기업생존: 우리나라기업을 중심으로

조승모 ( Seung Mo Cho ) 명지대학교 금융지식연구소 2010 금융지식연구 Vol.8 No.3

이 논문은 2002년 12월 현재 KOSPI 시장 및 KOSDAQ 시장에 상장된 우리나라 제조업체들을 대상으로 생존분석기법을 적용하여 각종 기업지배구조기제들이 기업의 생존성에 어떤 영향을 미치는지 살펴보았다. 실증분석결과, 소유가 집중되고 배당금을 많이 지급하는 기업의 생존성이 높은 것으로 나타났고, 내부자지분은 일정수준 이하에서는 기업생존성에 도움이 되지만 그 수준을 넘어서면 오히려 기업의 상장폐지를 촉진하는 것으로 나타났다. 채권자들의 감시기능은 자본성장성이 낮은 기업들에 한해서만 상대적으로 더 효과적인 것으로 나타났다. 또한, 통계적으로 약하게나마, 이사회규모가 작은 경우 이사회가 효과적인 장기 기업지배구조기제로 작동하는 것으로 나타났으며, 통계적으로 유의성이 낮은 결과이긴 하지만, 최적 이사회규모 또한 존재하는 것으로 확인되었다. This paper investigates into the effects of various corporate governance mechanisms on the corporate survivability by applying survival analysis techniques to Korean manufacturing firms listed in the KOSPI and the KOSDAQ markets as of December 2002. The empirical result shows that concentrated ownership and higher dividend payout contribute to longer firm survival while insider ownership, as it increases, at first contributes to firm survival and later promotes corporate delisting. The monitoring role of creditors has been confirmed only relatively more effective for firms with lower capital growth. In addition, smaller board size has turned out effective, although statistically weakly, as a corporate governance mechanism in the long run and there has proved to be an optimal level of board size although the statistical significance is rather weak.

병렬 객체지향 시스템의 검증

조승모(Seung Mo Cho),김영곤(Young Gon Kim),배두환(Doo Hwan Bae),변성원(Sung Won Byun),김상택(Sang Taek Kim) 한국정보과학회 2000 정보과학회논문지 : 소프트웨어 및 응용 Vol.27 No.1

모델체킹은 검증하려는 대상 시스템의 동작 모델이, 그 시스템이 만족해야 할 성질을 만족시키는지를, 시스템의 상태공간을 검사해 봄으로써 알아보는 정형 검증 기법의 하나이다. 이러한 모델체킹 기법을 병렬 객체지향 시스템에 적용하기 위해 기존의 모델체커인 SPIN에서 지원하는 모델링 언어인 Promela를 병렬객체지향 개념을 추가하여 확장한 언어인 APromela를 제안하였다. 이는 Promela가 프로세스를 단위로 하는 병렬성만을 지원하는데 반해, 액터 모델에 기반한 객체지향 병렬성을 지원한다. 또한 우리는 이 언어로 작성된 모델을 자동으로 Promela로 변환하는 규칙을 제안하였다. 이를 통해, 기존의 모델체커를 이용해 병렬 객체지향 시스템의 검증을 수행할 수 있다. 이 언어의 응용으로 UML 로 기술된 명세의 검증을 수행하는 과정을 제시하였다. Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by explorating the state space of the model.We apply model checking to the formal verification of the concurrent object-oriented system, using an existing model checker SPIN which has been successful in verifying concurrent systems. First, we propose an Actor-based modeling language, called APromela, by extending the modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization.Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. As an application of APromela, we suggest a verification method for UML models. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.

대학 금융수업에서 옵션 관계식의 효과적이고 효율적인 증명에 관한 연구

조승모 ( Cho Seung Mo ) 아시아문화학술원 2016 인문사회 21 Vol.7 No.4

본 논문에서는 대학의 금융수업에서 옵션과 관련된 관계식들을 보다 효과적이고 효율적인 방식으로 증명하는 방법에 관해 연구하였다. 풋-콜 패러티와 옵션 프리미엄의 범위와 같이 무차익거래 상태에서 성립하는 옵션 관계식들을 증명함에 있어, 주로 포트폴리오의 가치를 이용하는 증명방법과 차익거래의 현금흐름을 이용하는 증명방법이 널리 이용되는데, 본 논문에서는 이 두 가지 방법의 장점을 취하고 단점을 보완한 증명방법을 제시하였다. 차익거래의 현금흐름을 이용하는 증명방법에 특정한 형태의 표를 도입함으로써 증명과정이 비교적 단순하고 이해하기 쉬운 형태가 되도록 하는 동시에 차익거래와 차익을 한눈에 파악할 수 있도록 하였다. 이러한 증명방법은 비교적 쉬운 방식으로 옵션 관계식들을 증명할 수 있도록 할 뿐만 아니라, 차익거래를 구성하는 방법을 별도로 가르칠 필요가 없도록 함으로써 효과적이고 효율적인 수업을 가능하게 한다 하겠다. This paper has studied a method of effectively and efficiently proving option-related formulae in university finance lectures. There are two widely used ways of proving option-related formulae under absence of arbitrage such as the put-call parity and the bounds for option premiums: the one using portfolio values and the other using cash flows of arbitrage trades. We have suggested another way of proof for these formulae by taking the advantages and complementing the disadvantages of the two widely used proofs. By applying a certain form of table to the proof using cash flows of arbitrage trades, we have proposed a relatively simpler proof making the forms of arbitrage trades and arbitrage profits easier to grasp at first sight. Such a proof can make the relevant lecture more effective and efficient in that it proves the option-related formulae in a relatively easier way and that it does not require the instructor to teach how to form arbitrage trades regarding the formulae in addition to their proofs.