SC/ACSR : ACSR과 Statechart를 조합한 정형 명세

황대연(Dae Yon Hwang),김진현(Jinhyun Kim),최진영(Jin-Young Choi) 한국정보과학회 2011 한국정보과학회 학술발표논문집 Vol.38 No.1A

Statechart는 상태 기계를 기반으로 하는 정형 명세 언어로 반응형 시스템의 행위를 상태와 그 상태에서 받는 이벤트에 의한 전이로 표현한다. 프로세스 알제브라의 한 종류인 ACSR은 이벤트 기반으로 프로세스들 간의 통신과 프로세스의 우선 순위, 자원 소모 등의 표현이 용이한 정형 명세 언어이다. 본 논문에서는 서로 다른 관점의 명세를 하는 이 두 가지 언어가 서로를 보완하여 ACSR을 이용하여 Statechart의 공유 자원에 대한 사용과 제어를 표현하여 보다 시스템을 정확하게 명세할 수 있는 언어를 제시한다. 이를 위해 두 언어의 연결을 위한 정형적 문법과 의미를 제시한다.

Rhapsody Statecharts 의 정형검증을 위한 변환 알고리즘 연구

황대연 ( Dae Yon Hwang ),박승현 ( Seunghyun Park ),이나영 ( Na-young Lee ),김윤구 ( Yun Goo Kim ),최진영 ( Jin-young Choi ) 한국정보처리학회 2006 한국정보처리학회 학술대회논문집 Vol.13 No.2

Statechart 는 상태 기반의 시각적 명세 언어로 UML 에 포함되어 매우 널리 사용되고 있다. 하지만 UML 의 특성에 의해 그 의미론이 비정형적이 되었으며, 시스템의 행위를 불안하게 만드는 비결정적인 경우가 발생하게 된다. 본 논문에서는 UML 지원 도구인 Rhapsody 의 statechart diagram 중 코어 부분을 정형적 의미론을 가지는 명세로 변환함으로써 비결정적 명세를 찾아낼 수 있음을 보였 다.

Assertion Based Verification을 이용한 Statechart 모델의 검증

황대연(Dae-Yon Hwang),방기석(Ki-Seok Bang),최진영(Jin-Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅱ

Statechart는 매우 널리 쓰이고 있는 명세 언어이다. 현재는 UML에 포함되어 많은 사람들이 구현하고자 하는 시스템의 명세에 Statechart를 이용하고 있다. Statechart 명세는 구현될 시스템의 설계도 역할을 하기 때문에 오류가 있을 경우 매우 치명적일 수 있으며, 반대로 시스템의 오류를 명세 단계인 Statechart 명세에서 찾아내게 되면 수정에 필요로 하는 비용과 시간의 손실을 최소화 할 수 있다. 본 논문에서는 하드웨어 검증 분야에서 사용되고 있는 Assertion Based Verification (ABV) 방법론을 Statechart 영세에 적용하여 시뮬레이션 등으로는 찾아내기 힘든 오류를 찾아낼 수 있음을 보였다.

Statchart/ACSR:State chart와 ACSR을 조합한 정형 명세

황대연(Dae Yon Hwang),김진현(Jinhyun Kim),안영정(Young-Jung Ahn),강인혜(Inhye Kang),최진영(Jin-Young Choi) 한국정보과학회 2012 정보과학회 컴퓨팅의 실제 논문지 Vol.18 No.2

실시간 소프트웨어가 프로세스가 되어 운영체제 위에서 실행이 되면 소프트웨어의 기능만을 명세하는 것으로는 소프트웨어의 안전성을 보장할 수 없다. 때문에 소프트웨어가 올라간 플랫폼의 정보를 포함하여 명세하고 자원과 cpu에 대한 스케줄링 알고리즘도 살펴보아야 비로소 실시간 제약 사항을 만족하는지를 확인할 수 있다. UML에 포함되어 있는 Statechart 언어는 소프트웨어의 행위를 표현하기에 적합하지만 프로세스가 되어 스케줄링 되는 것을 표현하는 것에는 많은 제약이 존재 한다. 본 논문에서는 이처럼 Statechart로는 명세하기 어려운 부분인 자원과 통신에 관련된 특징을 ACSR을 통하여 명세하여 보완하고자 한다. 두 가지 정형 언어를 통해 보다 시스템을 정확하게 명세할 수 있는 방법을 제시하고, 이를 위해 두 언어의 연결을 위한 정형적 문법과 의미를 제시한다. For Real-time systems, formally specifying the functional behavior of the software and verifying it is not enough to prove that it will meet its real-time requirement. When a software is loaded as a process and gets restriction on resources, the platform information has to be considered together with the software. In this paper we propose a combination of two formal language, Statechart and ACSR to complement each other's weak point and to formally specify software and platform together.

SMV를 이용한 접근통제모델의 정형적 설계방법 연구

황대연(Dae-Yon Hwang),강인혜(Jin-Young Choi),강필용(In-Hye Kang),이완석(Pil-Yong Kang),최진영(Wan S. Lee) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ

컴퓨터 시스템에 대한 보안의 필요성이 계속적으로 증대되고 있으며 이에 다양한 보안시스템들이 개발되고 있다. 이러한 보안 시스템들이 높은 등급의 평가를 받기위해서는 정형적 방법론을 사용하여 명세 및 검증을 해야 한다. 본 논문에서는 정형 검증의 한 방법론인 모델 체킹을 이용하여 접근통제모델을 설계하고 검증하는 방법을 제안하고자 한다.

상염색체 우성 다낭신에서의 신낭종 경화요법

김연수(Yon Su Kim),안규리(Cu Rie Ahn),한진석(Jin Suk Han),김성권(Shung Gwon Kim),이정상(Jung Sang Lee),이중건(Jung Geon Lee),윤성철(Sung Chul Yoon),박종훈(Jong Hoon Park),송은경(Eun Kyong Song),황대연(Dae Yeon Hwang),박정환(Jung Hwan 대한신장학회 2002 Kidney Research and Clinical Practice Vol.21 No.4

배 경 : 상염색체 우성 다낭신(ADPKD)은 성인에서 가장 흔한 유전성 신질환의 하나로서 낭종의 팽창으로 인한 복부 팽만이나 통증을 흔히 호소한다. 이의 치료를 위해 에탄올을 이용한 경화요법이나 복강경을 이용한 치료, 수술적 감압술 등이 사용되어지고 있다. 본 연구에서는 한국인 ADPKD 환자에서의 경화요법 후의 임상경과를 분석하고, 새로운 경화제인 n-butyl cyanoacrylate(NBCA)의 유용성을 검토하였다. 방 법: 저자들은 한국인 ADPKD 환자 24명을 대상으로 에탄올경화요법(n=9) 및 NBCALipiodol 혼합액을 이용한 경화요법(n=18)(3예는 두가지 치료법 병행 )을 시술하고 이들의 임상 경과를 추적 관찰하였다. 결 과: 대상 환자의 남녀비는 8 : 16이었고 치료 시 평균연령은 50±13세였다. 경화요법의 적응증으로는 동통이 14예, 복부 팽만이 7예였으며, 흡인된 낭종의 직경은 5 내지 16 ㎝으로 다양하였다. 동통이나 복부팽만은 2명을 제외한 전원에서 주관적인 개선을 보였다. 시술 전후의 평균동맥압은 시술 전 112±11.1, 시술 후 1개월 96±9.6, 시술 후 6개월에 98±9.7 ㎜Hg로 유의한 저하를 보였으나(p<0.05), 이러한 효과는 12개월째에 소실되었다. 혈중요소질소 농도는 기저치와 시술 후 6개월 측정치 사이에 유의한 차이가 없었다[24±12.1 대 22±14.6(㎎/dL)]. 출혈이나 감염과 같은 주요 합병증은 발생하지 않았으며, 시술과 관련된 사망례도 없었다. 에탄올과 NBCA 사용군 사이에 치료효과나 합병증에서 차이는 관찰되지 않았다. 결 론: ADPKD 환자에서의 신낭종 경화요법은 대부분에서 증상의 완화를 보였고, 일시적인 혈압강하 효과를 보였으며, NBCA는 신낭종 치료에 새롭게 사용된 경화제로서 단기관찰 결과 유용하고 안전한 것으로 생각된다. Background : Autosomal dominant polycystic kidney disease(ADPKD) is the most common hereditary renal disease in adults, and its major complaints include pain and abdominal fullness due to cyst expansion. So far, for the control of these symptoms, cyst ablation with ethanol or tetracycline, laparoscopic manipulations and surgical marsupialization have been used. Methods : We used conventional ethanol(n=9) or n-butyl cyanoacrylate(NBCA) plus lipiodol solution (n=18) or both(n=3) for separate cysts as the sclerosing agent in 24 adult Korean ADPKD patients. And their clinical courses after treatment were evaluated. Results : The male to female ratio was 8 : 16 and the mean age at the treatment was 50 yrs(S.D. 13.1). Causes for aspiration were pain in 14 and abdominal fullness in 7 patients and the range for the cyst diameters aspirated were 5-16 cm. Flank pain or discomfort were decreased subjectively in most cases except two. Mean arterial pressures(S.D.) (㎜Hg) before and after procedure were as follows 112(11.1)(basal), 96(9.6)(1 month) and 98(9.7)(6 month)(p<0.05, paired-t test). Blood urea nitrogen levels(㎎/dL) were not changed 6 month later[24 (12.1) vs. 22(14.6)]. There was no major complication such as bleeding or infection and no death and associated with procedure. There was no difference of therapeutic effect according to sclerosing agent. Conclusion : NBCA was as effective as conventional ethanol for sclerotherapy in ADPKD and cyst ablation therapy showed a BP-lowering effect in short-term period.

GABA 함량이 높은 청국장을 발효하는 균주의 분리 및 동정

So-Yon Mann(맹소연),Eun-Ah Kim(김은아),Ga-Young Lee(이가영),Ro-Ui Kim(김로의),Dae-Youn Hwang(황대연),Hong-Joo Son(손홍주),Dong-Seob Kim(김동섭) 한국생명과학회 2013 생명과학회지 Vol.23 No.1

전통적인 방법으로 제조된 청국장으로부터 우수한 발효 균주들을 분리하여 재래식으로 청국장을 제조하고, 제조된 청국장의 생리활성 물질인 GABA를 유지 및 보강하면서 품질을 향상시키기 위하여 청국장 발효능이 뛰어난 종균을 찾아 분리하였다. 분리된 균주들 가운데 GABA의 함량이 높은 청국장을 생산하는 MC 31을 실험균주로 선택하였고 API Kit와 16S rDNA sequence를 통하여 Bacillus subtilisMC 31로 명명하였다. B. subtilisMC 31의 최적배지와 온도, 시간을 찾아본 결과 LB 배지에서 37℃, 24시간이 가장 높은 생육을 나타내었다. GABA 생산에 적합한 발효 온도와 시간을 조절하여 최적 조건을 찾아본 결과 B. subtilisMC 31는 40℃에서 72시간에 가장 많은 GABA를 생산하였다. To isolate GABA-producing microorganisms, 1,500 strains were isolated from different Chungkookjang samples and screened. From these strains, 20 were selected for further analyses based on a protease and slime-producing activity test. The MC 31 strain showed the highest GABA concentration in Chungkookjangand was used in this study. MC 31 was identified as Bacillus subtilisby an API 50CHB kit and 16S rDNA sequences analysis and named as B. subtilisMC 31. B. subtilisMC 31 showed exponential growth up to 12 hours at 37℃ in LB broth, and it reached a stationary phase after 24 to 36 hours of incubation. B. subtilisMC 31 showed maximum GABA content at 72 hours after incubation at 40℃.

B. subtilis MC 31를 이용한 청국장의 품질특성

맹소연(So-Yon Mann),김은아(Eun-Ah Kim),이가영(Ga-Young Lee),김로의(Ro-Ui Kim),황대연(Dae-Youn Hwang),손홍주(Hong-Joo Son),이병원(Byong-Won Lee),이충렬(Chung-Yeol Lee),김동섭(Dong-Seob Kim) 한국생명과학회 2013 생명과학회지 Vol.23 No.4

GABA 함량이 높은 청국장을 발효하는 Bacillus subtilis MC 31의 청국장 품질특성을 조사하였다. B. subtilis MC 31에 의해 발효된 청국장으로부터 24개의 아미노산이 검출되었고 그 중에서도 leucine이 가장 높은 함량을 나타냈다. B. subtilis MC31에 의해 발효가 된 청국장의 미생물의 생육 변화를 조사한 결과 총 균수가 정지기에 들어서면서 log 9.52±0.5~log 9.049±0.5 CFU/g까지 증가하였다. 청국장의 일반성분은 수분 61.7±0.01%, 회분 1.52±0.01%, 조단백 17.66±0.04%, 조지방 8.96±0.03%, 조섬유가 2.61%를 함유하였다. 암모니아태, 아미노태, 환원당은 모두 삶은 콩보다 청국장의 함량이 높게 조사되었지만 산도와 총 당은 청국장이 삶은 콩보다 함량이 낮았다. 청국장의 pH는 시간이 지날수록 알칼리화되고 점질물은 4.7±0.05%, protease activity는 0.519±7.36 g/l로 나타났으며 Fibrin plate와 Robbin실험을 통하여 fibrinolytic activity도 높음을 확인하였다. 이상의 결과로 미루어 보아 B. subtilis MC 31은 우수한 청국장 품질을 띄어 제조용 균주로 사용이 가능한 것으로 사료된다. Chungkookjang was fermented by B. subtilis MC31, a γ-amino butyric acid (GABA) producing microorganism. The characteristics of Chungkookjang were investigated while fermenting. Twenty four amino acids were detected in Chungkookjang, leucine was the highest of them all. Total cell populations of B. subtilis MC31 phase were between log 9.52±0.5 ~ log 9.049±0.5 CFU/g at stationary phase. Contents of moisture, crude ash, crude protein, crude lipid and crude fiber are 61.07±0.01%, 1.52±0.01%, 17.66±0.04%, 8.96±0.03% and 2.61%, respectively. Contents of ammonia type nitrogen, amino type nitrogen and reducing sugar were increased during fermentation at 40℃ for 72 hr, however those of titratable acidity and total sugar were decreased. pH was slowly alkalized during fermentation. Viscous substance and protease contents in Chungkookjang were 4.7±0.05% and 0.519±7.36 g/l, apiece. When the fibrin plate and Robbin method for fibrinolytic activity were applied, B. subtilis MC31 showed high activity. These results suggested that B. subtilis MC31 is suitable to be used as a starter to enhance the quality of Chungkookjang.

말기 신부전으로 진행하는 한국인 상염색체우성 다낭신 환자의 임상적 특성

황영환(Young Hwan Hwang),안규리(Cu Rie Ahn),황대연(Dae Yeon Hwang),이은주(Eun Joo Lee),어현선(Hyun Seon Eo),채희진(Hee Jean Chae),이정은(Jung Eun Lee),김연수(Yon Su Kim),한진석(Jin Suk Han),김성권(Suhng Gwon Kim) 대한신장학회 2001 Kidney Research and Clinical Practice Vol.20 No.2

말기 신부전은 상염색체우성 다낭신 환자의 가장 중요한 합병증이다. 상염색체우성 다낭신에서 말기 신부전증의 위험인자로는 PKD1 가계, 남성, 안지오텐신 전환효소 유전자의 다형성 등의 유전인자와 함께 고혈압, 빠른 발병연령, 육안적 혈뇨, 단백뇨 등의 비유전인자가 알려져 있다. 그러나 동양인을 대상으로 한 연구는 거의 없는 실정이다. 방법 : 연구자들은 우리 나라 상염색체우성 다낭신 환자에서 말기 신부전증의 빈도, 신부전증의 진행속도 및 위험인자를 알아보기 위하여, 서울대학교병원 다낭신 클리닉에 등록된 다낭신 환자 148명 중 말기 신부전으로 진행한 32명 환자들의 임상적 특징을 파악하고, 이를 신기능이 50세 이후에도 정상으로 유지되는 군 14명과 비교하였다. 결과 : 말기 신부전 환자 32명의 남녀 14:18명이었고, 진단 당시 중앙연령은 43세(범위22-65세), 말기 신부전 도달연령은 52.5세(28-73세)이었으며 진단으로부터 신대체요법 시작까지의 기간은 6년(0-30년)이었다. 신기능 감소 속도를 알아보기 위해서 분석이 가능하였던 말기 신부전 환자 18명에서 혈청 크레아티닌의 역수를 취하여 시간에 따른 감소율을 보았을 때 고질소혈증이 시작된 후에는 진단 연령이나 성별에 관계없이 매년 -0.073dL/mg/year(-0.046- -0.114dL/mg/year)의 일정한 속도로 감소되어 8.2년(5.2-13년)에 말기 신부전에 도달하였다. 대상환자군에서 육안전 혈뇨, 하루 1g 이상의 단백뇨, 요석, 상부요로감염, 고혈압, 간 낭종의 빈도는 각각 69, 54, 16, 29, 85, 85%이었다. 한편 84%에서 가족력이 있었고 이들 중 10%는 말기 신부전의 가족력이 있었고, PKD1:PKD2의 비율은 8명 중 7:1이었다. 이를 대조군과 비교하였을 때, 육안적 혈뇨와 단백뇨의 빈도가 신기능유지군에 비해 말기신부전 군에서 유의하게 높았다(각각p=0.001,p=0.0008), 한편 연관분석을 실시한 유지군 2명 중 1명은 PKD1, 1명은 PKD2였다. 결론 : 마기 신부전 환자 34명에서 신기능은 어느 연령까지는 유지되다가 일단 고질소혈증이 발생하면 일정한 속도로 신기능의 감소가 진행하여 8.2년에 말기 신부전에 도달하였다. 말기 신부전증의 임상적 위험인자로 육안적 혈뇨와 단백뇨가 확인되었다. End stage renal disease(ESRD) is a well-known major complication of autosomal polycystic kidney disease(ADPKD). Several risk factors of renal progression in ADPKD were identified, such as PKD1 gene, male gender and earlier age of onset. In Korea, ADPKD is a cause of ESRD in 2Yo of hemodi- alysis patients. Until now, only a few detailed studies have been performed in regarding to evaluate the risk factor for ESRD especially in the Asian population. 148 ADPKD patients were registered to PKD clinic in our hospital(Mar. 1996-Dec. 1999). Among them, 34 patients(male : female 14: 20) who had started renal replacement therapy were studied to elucidate clinical characteristics including the nature of progression of renal failure. These data were compared with 14 patients(male : female 3: 11) who did not develop renal failure(serum creatinine ≤1.4 mg/dL) at the age of 50 years. Median age at the diagnosis of ADPKD was 43 years(range : 22-65 years), median age at initiation of renal replacement therapy(RRT) was 52.5 years(28-73) and median duration from the diagnosis to RRT were 6 years(0-30). The prevalence of gross hematuria, proteinuria (>1g/24h), urolithiasis, upper urinary tract infection, hypertension and liver cysts were 69, 54, 16, 29, 85 % and 85%, respectively. 84% of these patients had family members with ADPKD and 10% of them had ESRD family members. PKD1 vs. PKD2 was 7: 1 in 8 patients with ESRD and 1: 1 in 2 patients of control group. Gross hematuria and proteinuria were more prevalent in ESRD patients than the control group(p=0.001 and p=0.0008, respectively). In 18 patients with ESRD, rates of renal progression were traced using a reciprocal of serum creatinine(1/Cr) curve. Once azotemia(serum creatinine value ≥1.5 mg/dL) developed, the median rate of decline of 1/Cr was -0.073dL/mg/year(range : -0.046--0.114dL/mg/ year), which was constant irrespective of either the age of onset or sex. In summary, in 34 patients, the renal function seemed to be maintained to a certain age. But, once azotemia developed, the renal function was rapidly declining with similar rate, ended up ESRD in 8.2 years. Presence of gross hematuria and proteinuria were associated with poor prognosis.

UPPAAL을 이용한 인공 심장 박동기의 안전성 검사

안소진(So Jin Ahn),황대연(Dae Yon Hwang),최진영(Jin-Young Choi) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1A

정형기법은 소프트웨어 및 하드웨어 시스템의 요구사항을 모순, 모호함 없이 정확하게 명세하고 검증할 수 잇는 방법으로, 안전성이 중요한 소프트웨어에 많이 적용되어 반드시 보장되어야 할 속성을 소프트웨어가 만족하는지 확인하는데 사용되고 있다. 본 논문은 정형기법 커뮤니티에서 선정한 여러 도전 과제 중 하나인 인공 심장 박동기(pacemaker)를 실시간 속성을 표현할 수 있는 정형기법 도구인 UPPAAL을 사용하여 모델링하고 주요 속성을 검증하였다. 이를 통해 실시간 속성으로 인해 명세 및 검증하기 힘든 소프트웨어에 정형기법을 적용하여 안전성을 확학인할 수 있음을 보인다.