{"entities":{"Q6535839":{"pageid":14146982,"ns":120,"title":"Item:Q6535839","lastrevid":103503689,"modified":"2026-06-06T07:30:16Z","type":"item","id":"Q6535839","labels":{"en":{"language":"en","value":"Applying formal verification to an open-source real-time operating system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7810661"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$7B9CE666-356C-4A76-86AE-7A0FAE150057","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"441c02441038561aec4b2030b347e145542c4917","datavalue":{"value":{"text":"Applying formal verification to an open-source real-time operating system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6535839$29322702-2274-4EC1-9CEB-011735E5C697","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"07f5129e4e7db25e30bb0b378de06aa43afdd9a4","datavalue":{"value":"1547.68107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$01A40174-DF20-468B-842C-111CAAA2EFCC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a13d22249556e6375ac022fed6601fa45134bfb","datavalue":{"value":"10.1007/978-3-031-40436-8_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$5C62ADBC-4D10-4B5A-AFC0-EAB112392AD8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bcc2517d7f29a0c99d871175f905014f619cab8","datavalue":{"value":{"entity-type":"item","numeric-id":539164,"id":"Q539164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$C61943A6-B222-4DC8-AC45-0C80FEF9609C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c1221725fb3e6959ea5910f15bf1bc2301913fba","datavalue":{"value":{"entity-type":"item","numeric-id":6535838,"id":"Q6535838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$7B0C291B-9FB7-4C68-ADB7-FFA1496407E5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1952080acac824c5abaf90b4ba5029824c97690c","datavalue":{"value":{"time":"+2024-02-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6535839$7EBC1989-B36C-437C-BDA2-4F3051973570","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$9691D0B6-B4CB-4335-A37B-B6C0DC668FAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$EAB1C851-19CD-4056-92AF-9D93B61CA3DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$937D2D69-CCC1-4D87-AE5B-EC11647954B0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"300ec1c5a0e877c96a727fb39c2706fae01eac67","datavalue":{"value":"7810661","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535839$EA58EC49-5EEF-41A5-B6DD-750E81EAB2AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d866d2f01ac2c31359811196209e4cb400acaa05","datavalue":{"value":"unifying theories of programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$BE093212-FC67-4C6C-BBDF-3D4A74725285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$4F81829C-33C0-4F9C-A643-C5A95A7424AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e16944d6d91b386448be2fb690b3d55ea295cfd4","datavalue":{"value":"Promela/SPIN","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$3D955A1C-078D-4D2B-BEB3-8CBBDA23B147","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"44bb8f04b1811f1c691fc7800979510b4e7dd1f3","datavalue":{"value":"test generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$8BD776E0-06C7-4C2F-BFE2-50D3C238E887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d9012e9ace873ca33308892db81c6b209fe7ec2","datavalue":{"value":"real-time operating systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$727A98A0-68FA-49DD-9CFF-AE4ACD7A3D94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6f492439882e7d67a3454f3982eeffcf241d91e","datavalue":{"value":"RTEMS","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535839$A4258C56-951E-4834-B61E-9455C28A04A8","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$D17A0B54-3F3D-4AB2-80F6-228638F0CE21","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b64342cfb9f84ce94653189292867c9c288ddaf","datavalue":{"value":{"entity-type":"item","numeric-id":2296283,"id":"Q2296283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$BEEBA647-0B09-42C1-84D0-9FD00063193C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a095f424b7b154d9ec141c33d84ba3688442215b","datavalue":{"value":{"entity-type":"item","numeric-id":1019021,"id":"Q1019021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$C5A96DD1-F59C-4184-A9FD-C15E5445A725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"261945cd779fe188f5776f40c42939a6d6f5c853","datavalue":{"value":{"entity-type":"item","numeric-id":3585021,"id":"Q3585021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$1A1609EA-5C4C-41D4-BC36-AED3A93A3421","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adc5ab3e12b39fe7ff128694a340cdf09c3b5bd1","datavalue":{"value":{"entity-type":"item","numeric-id":5045469,"id":"Q5045469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$B4191D81-E650-45A9-809D-F3C9243205E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"701136575d386e99fb6cc1edc1faab94513827a3","datavalue":{"value":{"entity-type":"item","numeric-id":3585022,"id":"Q3585022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$B69AC217-CA0E-4648-9305-D364F6CE2431","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf1fcaf801699e340ab052c7ce961980dd3177c0","datavalue":{"value":{"entity-type":"item","numeric-id":5307482,"id":"Q5307482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$56742339-69ED-49A2-A205-7668D0F0CC10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$67270910-1DF9-4760-BB8A-A706D973A85F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f65cf27cb319b50deacb73df4d115e078e49367","datavalue":{"value":{"entity-type":"item","numeric-id":2007732,"id":"Q2007732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$91C878B5-B7D9-44ED-9517-5596DD7D313B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"077ff53ae2b2205b555092a4a22f48106572ae4e","datavalue":{"value":{"entity-type":"item","numeric-id":5096726,"id":"Q5096726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$C0A7A096-6E0C-46FB-B86D-87E3E79F85A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ee72b851380674a3f91d5d9336820b8b7299f05","datavalue":{"value":{"entity-type":"item","numeric-id":3585019,"id":"Q3585019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$0A1C08B5-B40C-4310-A7D4-269EC0CDE8B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d223981ae7810a035830c0eb8a6cb984aabc840","datavalue":{"value":{"entity-type":"item","numeric-id":4536898,"id":"Q4536898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$6366420C-D3B9-4F78-A794-E2BA252845C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5caccfbbb6517f73e97dcb9e221bc0dc8ab8325b","datavalue":{"value":{"entity-type":"item","numeric-id":2842641,"id":"Q2842641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$213BDDA1-68B2-4930-B4A4-81CF53B11EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5de220317fd709a7e63acdecfb92f5c42b492","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$D031CD74-BAF8-4417-B29F-3E1DCBBB3933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f21ed24ea2d883ca70cb5f570bbcde52b53f24","datavalue":{"value":{"entity-type":"item","numeric-id":2198135,"id":"Q2198135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$4FF3FF88-A17C-47A6-A48F-B4BB8BC82663","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7055297a7b50a57f393bf91cddbacab39495edd","datavalue":{"value":{"entity-type":"item","numeric-id":4412559,"id":"Q4412559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$B8D3C675-52B4-4AEB-81C5-3272E5F9E6CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75927e1e47a95e29ccdd8f48ad53b644d7d6f434","datavalue":{"value":{"entity-type":"item","numeric-id":3585029,"id":"Q3585029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$05E5E119-2DF6-49A2-9B7A-F2837427601E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c891cbfb78fd1d255f13154316c326d70fd08978","datavalue":{"value":{"entity-type":"item","numeric-id":3585031,"id":"Q3585031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$3AD2F982-3A57-49E2-9C2D-F9EA5F930E33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4964dbcc2d6c924ffbfa971bd713c86d254ac017","datavalue":{"value":{"entity-type":"item","numeric-id":4787253,"id":"Q4787253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535839$54E4DB0D-77DB-431F-913D-2B27E12EC1AE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f5126bb604a2433d898f2d31c23ef8080bfb871","datavalue":{"value":{"entity-type":"item","numeric-id":903515,"id":"Q903515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1170b0f9efe89bc5829113cf149f0c8ecb2f053e","datavalue":{"value":{"amount":"+0.7507547736167908","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6535839$E566F3B2-B1A1-4498-9B97-8FB72DC6EDF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"086c1690d82047a205870680dca3d0ad18da1c18","datavalue":{"value":{"entity-type":"item","numeric-id":6535218,"id":"Q6535218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc569c1ab03454c45df5af9baa72ecd0c3529d59","datavalue":{"value":{"amount":"+0.7332450747489929","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6535839$345E4BBF-DB3B-41CF-84D2-B9FD1A655B8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80e1e080e49bf76f9e6ed75c07b07054e8f9a036","datavalue":{"value":{"entity-type":"item","numeric-id":2763995,"id":"Q2763995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"854316a679d14ccce6f8839977b78c6e485f54e1","datavalue":{"value":{"amount":"+0.7109400629997253","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6535839$4C128222-ECBD-4DD8-8CD1-D318494593E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f28dfd11ce40ef0b1453bf37d25eedb1598b1f9a","datavalue":{"value":{"entity-type":"item","numeric-id":465680,"id":"Q465680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dab2577248b9a1b0a8c5fdf7994e81594a7c83d7","datavalue":{"value":{"amount":"+0.709111750125885","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6535839$7797280D-57EC-4BC8-A7B3-CCD357975DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc452a87a25e174253c7287851cab47516a32457","datavalue":{"value":{"entity-type":"item","numeric-id":1395689,"id":"Q1395689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"feacbbd29856d8f3b6fc0c9151a05e6e31979f9f","datavalue":{"value":{"amount":"+0.7063086032867432","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6535839$5F121942-3FC1-4E1E-852E-F2B308032973","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Applying formal verification to an open-source real-time operating system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Applying_formal_verification_to_an_open-source_real-time_operating_system"}}}}}