합금에서 HTTP 전환 시스템 모델링

Question

HTTP 상호 작용, 즉 HTTPRequest/HTTPResponse 시퀀스를 모델링하고이를 전환 시스템으로 모델링하려고합니다. 내가 사용하여 클래스 상태에 순서를 정의 : 국가는 단순히 메시지의 집합입니다

open util/ordering[State] 

:

sig State { 
    msgSet: set Message 
} 

의 각 쌍 (HTTPRequest-> HttpResponse에) 및 (HTTPResponse-> HTTPRequest)은 전환 시스템에서 규칙으로 표시됩니다. 규칙은 하나의 상태에서 다른 상태로 이동하게하는 술어로서 합금에서 표현됩니다.

pred rsp1 [s, s': State] { 
    one msg: Request, msg':Response | (

     // Preconditions (previous Request) 
    msg.method=get && 
    msg.address.url=sample_com && 

     // Postconditions (next Response) 
    msg'.status=OK_200 && 

     // previous Request has to be in previous state 
    msg in s.msgSet && 
     // Response generated is added to next state 
    s'.msgSet = s.msgSet + msg' 
} 

불행하게도, 생성 한 모델이 너무 복잡 할 것 같다 :

예,이 특정의 HTTPRequest를 수신 한 후 HttpResponse에를 생성하는 규칙입니다 우리는 하나보다 규칙 다스 (더 복잡한이 위와 같지만 같은 패턴을 따른다.) 실행은 매우 느리다.

편집 : 특히 CNF 생성은 매우 느리며, 해결에는 상당한 시간이 걸립니다.

비슷한 전환 시스템을 모델링하는 방법에 대한 의견이 있으십니까?

대단히 감사합니다!

Answer 1

인상적인 세부 묘사가있는 모델입니다. 그것을 공유해 주셔서 감사합니다!

을 제외하고 다양한 형태의 honestAction은 그 자체로 인스턴스를 찾는 데 2 ​​~ 3 분이 걸리지 않으며 (경우에 따라 인스턴스를 찾지 못할 수도 있습니다.) 내가 멈추기 전에 15 분 정도 뛰었다.).

은 그래서 당신이 관찰하는 긴 CNF 준비 시간은 분명히 시간 문제를 야기하거나 honestAction 조건, 또는 (C) 모두에서 분리의 (b)의 크기에있어 하나의 (a) 단지 술어 rsp8에 의해 발생합니다.

시간 문제가 모델을 채우는 데 필요한 개인의 수와 모델의 제약 조건 수의 조합 폭발로 인해 발생했다고 의심 스럽지만 증명하지는 못했습니다.

내 첫 번째 본능은 모델의 세부 수준, 특히 추상 서명을 인스턴스화하는 많은 수의 싱글 톤 시그니처를 줄이는 것입니다. 이것들은 부기 목적으로 존재할 수있는 것 같아서 (어떤 규칙이 한 국가에서 다른 국가로의 전환을 허가 하는지를 확인할 수 있습니다), 또는 모델 작성자가 Alloy가 UserName과 같은 서명의 구체적인 인스턴스를 생성하는 것을 신뢰하지 않기 때문에, 암호, 코드 등

모델이 이제 제약 조건을 정의하고 합금이 작업을 수행하는 대신 특정 사례에 관련된 모든 개인을 정의하는 작업이 많은 것처럼 보입니다. 예를 찾는 것. (합금을 사용하여 속성을 확인하면 구체적인 예가 유용 할 수 있지만 다른 방법이 있습니다.)

모델의 많은 구체적인 서명이 싱글 톤 카디널리티로 제한되어 있으므로 모델 정의가 모델을 더 복잡하게 만드는 작업을한다는 것을 실제로 알지 못합니다. 내가 아는 한 모두, 그것은 그것을 더 간단하게 만든다. 그러나 본능적으로 본다면, 상태 변환은 호스트, 사용자 및 URI가 무엇이든지 관계없이 일반적으로 특정 속성을 가짐을 알기 쉽고 (합금이 설정하는 것이 더 쉽다는 것을 아는 것이 더 유용하다고 생각하는 것입니다) 호스트가 examplecom이고 주소 URI가 example_url_https 인 모든 경우에 해당 속성 rsp1이 적용됩니다.

I는 존재와 특성을 규정하는 개인들의 수와 개인이 상태 전이에 관여 할 수있는 제약을 줄이면 CNF 생성 시간을 줄일 수 있음을 추측.

주어진 장기간의 상태 전환을 테스트하여 주어진 시작 지점에서 특정 주 (또는 종류의 주)에 도착할 수 있는지 여부를 테스트하려는 경우 다시 생각해야 할 수도 있습니다 작업을 수행하기 위해 더 짧은 상태 전환 순서를 가능하게하는 접근법.

두 번째 추측은 모델의 구조 조정이 덜 필요합니다. 나는 완전히 이해하고 있다고 생각하지 않기 때문에, 의 수치화가 대신에 some 대신 명시 적으로 몇 가지 변수를 수량화하는 것이 다루기가 어려워서 문제가되는 것으로 판명 된 this example과 같이 성능을 향상시키는 데 도움이되는 것처럼 보일 때가 있습니다.

이 질문은 전체적으로 모델이 아닌 술어에서의 부량을 포함하며, 처음에는 one을 사용하는 정량화가 의도되지 않았으므로 여기서는 관련이 없습니다. 그러나 one 키워드의 효과를 간단한 방법으로 테스트 할 수 있습니다. 의 모든 것을 주석 처리하고 rsp8을 제외한 모든 단어를 주석 처리하고 one의 항목이 주석 처리 된 후 한 번만 사용하여 범위 8에서 술어 first != last을 실행했습니다. 그 키워드 그대로. one 키워드가 주석 처리 된 상태에서 Analyzer는 24 초 내에 문제를 실행했습니다. one 키워드를 제자리에 놓은 상태에서 500 초 동안 실행되어 포인트가 작성되고 종료되었다고 결정하기 전까지 실행되었습니다.

그래서 인스턴스 고유의 개체가있는 모든 시그니처에서 키워드 one을 제거하고 get, post, OK_200 등 및 appData에만 남겨 둡니다. 나는 또한 run 명령에서 키, 세션 ID, URL, 호스트, 사용자 이름 및 암호의 다양한 하위 유형을 사용하지 않거나 적어도 카디널리티를 제한하려고 시도합니다.