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,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과 분석기법의 적용성을 보였다

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

조승모 ( Seung Mo Cho ),이필상 ( Phil Sang Lee ) 한국금융공학회 2011 금융공학연구 Vol.10 No.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 ) 인문사회 21 2016 인문사회 21 Vol.7 No.1

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.

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

조승모(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 ) 포스코경영연구원 2011 POSRI경영경제연구 Vol.11 No.1

본 연구에서는 비상장 외국인투자법인에 투자한 외국인투자자들의 경영능력을 검증한다. 2009년 12월말 기준 12월 결산 비상장 외국인투자법인 자료를 다변량회귀모형, 순위프로빗모형 및 순위로 짓모형을 이용하여 분석한 결과, 외국인투자자의 비중이 높은 기업일수록 경영성과 및 신용도 측면에서 기업성과가 우수한 것으로 검증되었다. 이는 외국인 투자자가 선진적인 경영기법 및 발달된 경영자 감시기법을 통해 대리인 문제를 해소하고 기업경영을 효율화한다는 기존 연구들의 주장과 일치하는 결과이다. 이러한 결과는, 기업경영성과를 측정하는 측정치를 바꾸거나, 신용도를 분석하는 분석모형을 바꾸는 경우에도 일관되게 유효한 것으로 나타나, 그 강건성 또한 검증 되었다고 할 수 있다. This paper investigates the managerial capability of foreign investors for nonlisted foreign-invested corporations in Korea. To this end, we analyze the December 2009 data for nonlisted foreign-invested companies with fiscal year ending at the end of each December. Applying the multivariate regression model, the ordered probit model, and the ordered logit model to our data, we have verified that a higher share of foreign investors leads to a higher corporate performance in both managerial performance and credit ranking. This is consistent with previous literature asserting that foreign investors mitigate the agency problem and enhance the corporate performance with advanced managerial and monitoring skills. Moreover, this result has turned out to be robust across different measures of managerial performance and different models of credit analysis.

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

조승모 ( 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.

외국인투자자의 경영능력 검증: 비상장 외국인투자법인을 중심으로

조승모 ( Seung Mo Cho ) 포스코경영연구원 2011 POSRI 경영경제연구 Vol.11 No.1